726 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Guillaume ALLAIS	bd14d37ddc	[ fix ] make some exports public	2020-07-03 12:01:09 +01:00
Jan de Muijnck-Hughes	5abf053818	Fixed visibility of some list functions.	2020-07-03 11:59:55 +01:00
Niklas Larsson	c0e535516c	Merge pull request #380 from chrrasmussen/add-docs-about-dirs ... Add documentation for sourcedir/builddir/outputdir	2020-07-02 00:16:23 +02:00
Niklas Larsson	3507512e49	Merge pull request #401 from melted/buffer_has_io ... Convert Data.Buffer to HasIO	2020-07-02 00:01:28 +02:00
Christian Rasmussen	b4ba476c8a	Merge branch 'master' into add-docs-about-dirs	2020-07-01 23:51:40 +02:00
Niklas Larsson	f54ebcb3b1	Merge pull request #391 from ska80/upd-docs ... Update docs	2020-07-01 23:47:16 +02:00
Niklas Larsson	6673f49731	Convert Data.Buffer to HasIO	2020-07-01 23:33:30 +02:00
André Videla	5996361488	Update INSTALL.md ... Fix typo on INSTALL.md	2020-07-01 18:15:49 +01:00
André Videla	cec56561c6	Merge pull request #387 from LibreCybernetics/fix-export-vect ... Make Applicative implementation of Vect n public export.	2020-07-01 17:26:08 +01:00
Edwin Brady	c4d56e5481	Merge pull request #396 from edwinb/lazy-lazy ... Don't commit to a Force too early	2020-07-01 12:29:52 +01:00
Edwin Brady	e7830b2b40	Merge github.com:idris-lang/Idris2 into lazy-lazy	2020-07-01 11:59:35 +01:00
Edwin Brady	c216e1c560	Update test output	2020-07-01 11:53:06 +01:00
Edwin Brady	0d4db3ee75	Add 'force' and 'delay' as functions ... Since Force and Delay are keywords now, these may help in higher order cases in particular.	2020-07-01 11:35:27 +01:00
Edwin Brady	669e50ff55	Remove my debugging noise from test case	2020-07-01 00:43:33 +01:00
Edwin Brady	25491060e2	Don't commit to a Force too early ... If we have a delayed thing, but we don't yet know the expected type, don't commit to forcing because the expected type might turn out to be a delay. Fixes #395	2020-07-01 00:40:44 +01:00
Mark Barbone	4916dd23a9	Make Data.Vect linear (#333)	2020-06-30 15:05:19 +01:00
Kamil Shakirov	f094a52ba9	Update docs	2020-06-30 18:44:36 +06:00
Denis Buzdalov	df60e07962	List's snoc injectivity property was renamed approporiately.	2020-06-30 13:18:42 +01:00
Edwin Brady	393c1ed464	Merge pull request #388 from edwinb/samples-dir ... Copy samples directory from Idris2-boot	2020-06-30 11:23:40 +01:00
Edwin Brady	4f10bfcfd2	Copy samples directory from Idris2-boot ... This is referred to in the documentation, so should be there	2020-06-30 10:51:09 +01:00
Fabián Heredia Montiel	e488c6cf0e	Make applicative implementation of Vect public export	2020-06-29 18:27:57 -05:00
Niklas Larsson	53621f84c5	Merge pull request #370 from ShinKage/ansi ... Adds ANSI codes support in contrib	2020-06-29 19:43:46 +02:00
Edwin Brady	a35965be84	Merge pull request #384 from edwinb/unify-invert ... Use 'unify' rather than 'convert' if possible	2020-06-29 16:22:31 +01:00
Edwin Brady	a52308d77d	Add test files	2020-06-29 15:13:42 +01:00
Edwin Brady	ffbea6d160	Use 'unify' rather than 'convert' if possible ... 'convert' doesn't solve holes, so might reject things that are solvable. This can be an issue when resolving interfaces, because we were using convert for arguments of the invertible holes that arise when trying to resolve them. Fixes #66.	2020-06-29 15:04:32 +01:00
Edwin Brady	84477adfc9	Merge pull request #383 from edwinb/coverwhere ... Pay attention to nested names in coverage check	2020-06-29 13:52:32 +01:00
Edwin Brady	b2da2fe558	Pay attention to nested names in coverage check ... Fixes #164	2020-06-29 13:27:00 +01:00
Niklas Larsson	4db58171f9	Merge pull request #381 from chrrasmussen/avoid-traversing-modules-twice ... Avoid traversing all Idris modules twice when installing	2020-06-29 12:03:08 +02:00
Edwin Brady	31b486c8ed	Merge pull request #382 from edwinb/linear-holes ... Use precise inference for hole types	2020-06-28 23:17:59 +01:00
Edwin Brady	cc03a4cb3b	Add missing test file ... Apparently I forgot the input for linear012. Oops!	2020-06-28 22:28:56 +01:00
Edwin Brady	ff7d3a0246	Use precise inference for hole types ... That is, don't generalise multiplicities, because we need the hole type to be precise wrt multiplicities. Resolves #189	2020-06-28 22:16:15 +01:00
Christian Rasmussen	24bb84fcf5	Avoid traversing all Idris modules twice when installing	2020-06-28 21:36:48 +02:00
Christian Rasmussen	3bf384860a	Add documentation for sourcedir/builddir/outputdir	2020-06-28 19:56:02 +02:00
Edwin Brady	e175bb8310	Merge pull request #379 from edwinb/interface-type ... Record implicit parameters of interfaces	2020-06-28 15:31:47 +01:00
Edwin Brady	8ddac9c1d5	Record implicit parameters of interfaces ... We need to make sure they are inferred again when elaborating methods, so substitute in a _ in method types before substituting in the explicit parameters. In future, it might (probably will) also be useful to allow giving the implicit parameters explicitly when defining implementations. Fixes #374	2020-06-28 14:58:57 +01:00
Niklas Larsson	cd777a00ce	Merge pull request #376 from andrevidela/kleisli-arrow ... Add Kleisli arrow operators to contrib	2020-06-28 00:18:04 +02:00
André Videla	8d04881356	Add Kleisli arrow operators to contrib	2020-06-27 22:02:05 +01:00
Edwin Brady	fb9f79e3c6	Merge pull request #375 from edwinb/interactive ... Add new clause at next blank line	2020-06-27 21:36:59 +01:00
Edwin Brady	17fec60d7a	Add new clause at next blank line ... This fixes a thing that's been annoying me in the vim mode. It's usually something that's left to the editor, but we do all the work for the vim mode! (This is hard to test conveniently, sorry...)	2020-06-27 21:09:03 +01:00
Edwin Brady	35e328a505	Merge pull request #373 from edwinb/interactive ... Various interactive editing improvements	2020-06-27 19:10:16 +01:00
Edwin Brady	929c5504c5	Implement make-case	2020-06-27 18:28:09 +01:00
Edwin Brady	c043fc3c57	Do make-with IDE command properly ... Now updates the file rather than just printing the output, in update mode. Also adds bird tracks where appropriate in literate mode.	2020-06-27 17:06:17 +01:00
Edwin Brady	1b695bcc52	Display binder if it's not implicitly bindable ... This is particularly important if we're generating something that needs to be parsed and checked again. Fixes #185	2020-06-27 16:26:34 +01:00
Ohad Kammar	f31318f5e6	Merge pull request #372 from ohad/export-length-correct ... Export the `lengthCorrect` proof, as users might want to use it	2020-06-27 16:21:04 +01:00
Ohad Kammar	6683a2147f	Export the lengthCorrect proof, as users might want to use it ... Change the `len` to be irrelevant, as it's uniquely determined by matching on the input vector	2020-06-27 15:54:35 +01:00
Edwin Brady	6c007fc046	Use full names for constructors in case split ... Fixes #184	2020-06-27 15:47:38 +01:00
Ohad Kammar	574524d8de	Merge pull request #368 from ohad/fstrings ... Add a simple DYI f-string / string interpolation library	2020-06-26 21:12:13 +01:00
Giuseppe Lomurno	28018d9573	Fixed typo	2020-06-26 21:26:36 +02:00
Giuseppe Lomurno	36c62c754a	Updated documentation	2020-06-26 19:16:14 +02:00
Giuseppe Lomurno	5ccc6a397d	Added Control.ANSI module in contrib	2020-06-26 19:10:02 +02:00