Edwin Brady
d666ed50c9
A couple of library functions
2020-03-19 22:14:48 +00:00
Edwin Brady
b5b9372fff
Add delete and union to Data.List
2020-03-10 14:52:46 +00:00
Edwin Brady
625027f278
Add nub to Data.List
2020-02-09 21:45:36 +00:00
Edwin Brady
6f4fa7ade9
More Data.List functions
2020-02-01 13:32:30 +00:00
Edwin Brady
7d47c08140
Add Data.List.isPrefix
2020-02-01 12:57:14 +00:00
Alex Gryzlov
ce15b48a78
Merge remote-tracking branch 'upstream/master' into misc-fixes
2020-01-15 22:52:38 +01:00
Edwin Brady
050fcfa45a
Merge pull request #148 from msmorgan/list-replicate
...
Add replicate to base/Data.List.
2019-12-06 10:59:12 +00:00
Edwin Brady
468555bb2e
Merge pull request #143 from ohad/bugfix-#133
...
Bugfix #133 and library support for tail-recursive list manipulation
2019-12-06 10:56:03 +00:00
Edwin Brady
262177016c
Merge pull request #147 from msmorgan/list-zip
...
Add zip functions to base/Data.List.
2019-12-06 10:42:11 +00:00
Edwin Brady
d9f1b01ef7
Merge branch 'master' into bugfix-#133
2019-12-06 10:28:07 +00:00
Alex Gryzlov
f0ca75b537
add some lib fuctions from Idris1
2019-11-12 15:58:21 +03:00
Michael Morgan
9190ccf883
Add replicate to base/Data.List.
2019-10-29 16:08:13 -07:00
Michael Morgan
2a014d1e19
Add zip functions to base/Data.List.
...
This includes the following functions: zipWith, zip, zipWith3, zip3
2019-10-29 15:51:15 -07:00
Ohad Kammar
fd980bc92f
Add tail-recursive versions for most of the Data.List functions
...
Also include proof the tail-recursive versions are extensionally equivalent to the non-tail-recursive one
I'm a bit worried that some of those proofs came through, as
visibility modifiers should get in the way. If they cause problems at
some future point, just delete/comment them out.
2019-10-27 04:07:01 +02:00
Michael Morgan
e6121e0935
Remove trailing whitespace from Idris sources.
...
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
2019-10-25 14:24:25 -07:00
Michael Morgan
33110d1cda
Add head and tail to base/Data.List.
...
These functions use the NonEmpty predicate type in order to prove
that the operation will be valid.
Implementations copied from Idris1's Prelude.List module, except without
expanding the auto implicit argument.
2019-10-16 15:49:52 -07:00
Edwin Brady
bb6d0e07a7
Fix pruning ambiguities under 'Delayed'
...
Need to strip the 'delayed' or we'll miss some things
2019-10-13 17:09:31 +01:00
Edwin Brady
6cebc5ca4f
Add some handy list functions/properties
2019-10-13 13:59:42 +01:00
Edwin Brady
519415f82f
Add decidable equality for List
2019-10-10 17:38:09 +01:00
Arnaud Bailly
02978c81fc
Merge branch 'master' of https://github.com/edwinb/Idris2 into network-lib
2019-07-27 17:27:49 +02:00
Alex Gryzlov
b9b41dea40
port Data.List
2019-07-24 16:11:27 +03:00
Arnaud Bailly
7f53d0d54d
add 'missing' functions into base libraries
2019-07-23 09:37:48 +02:00
Edwin Brady
ccc53813ca
Initial attempt at RHS with application
...
Still some details to finish, plus testing, plus adding View modules to
the base libraries, but the basic idea works.
2019-07-07 00:07:59 +01:00
Edwin Brady
c02da23c1a
Add sort and merge to Data.List
2019-07-06 13:56:57 +01:00
Edwin Brady
e526badfe2
Delay case elaboration
...
This helps a few things because it delays elaboration of the block until
as much as possible is known about its type.
Also added a few libraries.
2019-07-02 16:53:41 +01:00
Edwin Brady
c121910298
Add 'base' libraries
2019-06-15 11:54:22 +01:00
