G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' ( #1093 )
2021-03-01 08:29:43 +00:00
Denis Buzdalov
7a8c12771b
[ base ] A property of interaction between zipWith and index ( #1128 )
2021-03-01 08:29:17 +00:00
Edwin Brady
4726c32d94
Add --ignore-missing-ipkg flag
...
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.
We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
2021-02-27 19:39:47 +00:00
Edwin Brady
37cc095f7a
Merge github.com:idris-lang/Idris2 into versions
2021-02-27 18:00:18 +00:00
Edwin Brady
1052c41a3c
Use version number field in ipkg
...
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
2021-02-27 14:15:19 +00:00
André Videla
aa27ccbdb6
Merge pull request #1097 from andylokandy/multiline
...
Implement multi-line string
2021-02-26 21:50:54 +00:00
G. Allais
59de5f1326
[ fix #762 ] Different case tree building strategy ( #1125 )
2021-02-26 09:33:07 +00:00
claymager
33e336ad27
Give App1 implementation of (>>) ( #1122 )
2021-02-25 17:09:24 +00:00
Andy Lok
5fed5c2b7a
Merge branch 'master' of https://github.com/idris-lang/Idris2 into multiline
2021-02-25 19:52:42 +08:00
Denis Buzdalov
874496e1ae
[base] Constructor's injectivity proofs for Exists and Subset ( #1118 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-02-24 19:11:41 +00:00
Denis Buzdalov
69be8f2102
[base] bimap functions were added for dependent pairs.
2021-02-24 16:41:33 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) ( #1095 )
2021-02-24 11:07:16 +00:00
Mark Barbone
0f7fa149c7
Make zip infixr 6
2021-02-23 10:54:28 +00:00
Denis Buzdalov
95af3cf4be
More compose instances and one usage of them ( #1089 )
2021-02-23 10:53:43 +00:00
Guillaume ALLAIS
00067e8151
[ fix #637 ] force indentation after a with
2021-02-23 10:52:22 +00:00
Donovan Crichton
1b9a220c42
Added comment descriptions for FC and FilePos.
2021-02-22 09:55:34 +00:00
G. Allais
74b051589b
[ new ] Perfect binary trees ( #1063 )
2021-02-22 09:54:16 +00:00
G. Allais
30d402ed7f
[ fix #899 ] Be careful when generating an impossible LHS ( #1081 )
2021-02-22 09:53:30 +00:00
Andy Lok
22a769e6b5
Implement multiline string
2021-02-20 18:05:26 +08:00
Mathew Polzin
d5d0b64b4a
withFile & writeFile cleanup ( #1085 )
2021-02-18 17:51:45 +00:00
Mathew Polzin
9f8a8b5d76
Add a total way of reading files in. ( #1070 )
2021-02-18 11:13:25 +00:00
Denis Buzdalov
b355b12cdb
Some cleanup was done. Changed code is mosly equivalent to the former.
...
A lot of useless matches of implicit arguments were removed.
2021-02-16 19:05:33 +00:00
Denis Buzdalov
0ac34538ec
A function from Not (x = y) to decEq x y = No _ was added.
2021-02-16 12:43:50 +00:00
Denis Buzdalov
4f28b92a19
Zero quantities were added to some interface usages.
2021-02-12 20:51:13 +00:00
Denis Buzdalov
123fbb7f33
weakenN's n parameter was made to have zero quantity.
2021-02-09 14:15:59 +00:00
SmiVan
952e20cc57
IOArray.fromList moved to HasIO
2021-02-06 20:37:15 +00:00
Wen Kokke
bd683938bf
Overhaul of concurrency primitives ( #968 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-02-05 16:16:20 +00:00
GustavoMF31
7f495999bd
Make :typeat a useful command ( #998 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-02-05 16:15:40 +00:00
Denis Buzdalov
5beda25da6
Seemingly outdated and non-typechecking module was removed.
2021-02-01 16:10:54 +00:00
Kamil Shakirov
173edb14a6
Remove unused modules
2021-02-01 14:26:18 +00:00
Stefan Hoeck
39824c6295
[new] Add Colist and Colist1 to base ( #997 )
2021-02-01 10:27:07 +00:00
Stiopa Koltsov
cff7db38cb
Control.App: use new type instead of Void as marker for I/O
...
Took me some time to figure out that `Void` means `IO`.
Express that knowledge more explicitly.
2021-01-31 11:58:10 +00:00
Andy Lok
5b367da2c9
[ refactor ] Rename Data.Strings to Data.String (1/2) ( #987 )
2021-01-27 19:18:34 +00:00
Kamiλ Shakirov
140879f7b9
[ new ] Zippable interface ( #990 )
2021-01-27 18:23:08 +00:00
Kamiλ Shakirov
3bbf52025a
Add zip*/unzip* for List1 ( #986 )
2021-01-26 10:39:16 +00:00
Rodrigo B. de Oliveira
dbea094a31
Fix Language.Reflection definition of INamespace
...
Fixes #943
2021-01-22 18:10:01 +00:00
mapf0ld
e15b1f0c78
[ refactor ] ltrim in terms of asList ( #894 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-01-22 15:07:23 +00:00
Kamil Shakirov
b540313c57
Add unzipWith and unzipWith3 for Stream
2021-01-22 10:41:16 +00:00
Kamil Shakirov
29cd9e86ec
Add unzipWith and unzipWith3 for Vect
2021-01-22 10:41:16 +00:00
André Videla
60527d127f
Merge pull request #554 from Sventimir/validation
...
Input validation
2021-01-22 01:30:07 +00:00
G. Allais
af94feb18e
Merge pull request #960 from stefan-hoeck/transformer-overhaul
2021-01-21 16:30:59 +00:00
Kamiλ Shakirov
db30dd3f16
Port Data.List.unzip from Idris1 ( #972 )
2021-01-21 16:30:00 +00:00
André Videla
0c665bc952
Merge pull request #884 from mattpolzin/list-reverse-involutory
...
Add proof that list reverse is involutive into base.
2021-01-21 13:33:34 +00:00
Jakub Okoński
1376bdf3f2
libs: mark Data.Nat.lteAddRight as public export
2021-01-21 12:40:17 +00:00
Stiopa Koltsov
0d363c9732
Add isYes function and friends
...
Added several functions for `Dec`. The set of functions and names
are picked consistently with `Maybe`:
* `isNothing` -> `isNo`
* `isJust` -> `isYes`
* `IsJust` -> `IsYes`
* `isItJust` -> `isItYes`
This is follow-up to #942
2021-01-21 12:36:02 +00:00
stefan-hoeck
92b9833ee2
fixed doc for WriterT
2021-01-21 13:25:48 +01:00
stefan-hoeck
fd4851c0f5
strict, not stricht
2021-01-21 13:24:40 +01:00
Stefan Hoeck
fb08004041
removed trailing whitespace ( #955 )
2021-01-21 11:33:03 +00:00
stefan-hoeck
d36a234041
finished MonadRWS
2021-01-20 05:58:19 +01:00
stefan-hoeck
e906b28cae
removed MonadState functions from RWS.CPS.idr
2021-01-20 05:51:39 +01:00
