Leonardo de Moura
|
87d97c24a7
|
chore: code convention
|
2020-11-19 08:13:11 -08:00 |
|
Leonardo de Moura
|
7e533b4650
|
refactor: use Lists for Array reference implementation
Motivation: better reduction in the kernel.
cc @Kha
|
2020-11-17 17:05:53 -08:00 |
|
Leonardo de Moura
|
8c4ac7ccc1
|
refactor: rename LeanInit ==> Meta, and reduce dependencies
|
2020-11-13 16:00:31 -08:00 |
|
Leonardo de Moura
|
65dafaf07c
|
fix: stdlib and tests
We also declare a few macros for the syntax command.
|
2020-11-12 07:12:30 -08:00 |
|
Leonardo de Moura
|
2537a2b84a
|
chore: implement list and array literals using syntax command
|
2020-11-11 13:50:25 -08:00 |
|
Leonardo de Moura
|
cca3bad0bb
|
feat: add Prelude.lean
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
|
2020-11-10 18:08:18 -08:00 |
|
Leonardo de Moura
|
c665d5e20a
|
chore: cleanup
|
2020-11-10 15:40:00 -08:00 |
|
Leonardo de Moura
|
2d2d39c78e
|
chore: use mut
|
2020-11-07 17:32:13 -08:00 |
|
Leonardo de Moura
|
bf4d48f348
|
chore: cleanup for presentation
|
2020-11-05 12:43:02 -08:00 |
|
Leonardo de Moura
|
8c9f148e2f
|
chore: use new termFor, termReturn, termTry, and tryUnless
|
2020-10-31 19:19:18 -07:00 |
|
Leonardo de Moura
|
131cb7036f
|
feat: add combinators for Subarray
|
2020-10-28 19:49:38 -07:00 |
|
Leonardo de Moura
|
4ba21ea10c
|
chore: cleanup src/Array/Basic.lean
|
2020-10-28 19:35:42 -07:00 |
|
Leonardo de Moura
|
6765440724
|
chore: remove clutter
|
2020-10-28 14:11:06 -07:00 |
|
Leonardo de Moura
|
3e6b2964cf
|
chore: minor cleanup
|
2020-10-28 13:18:45 -07:00 |
|
Leonardo de Moura
|
898a08a0c1
|
chore: avoid Has prefix in type classes
closes #203
|
2020-10-27 18:29:19 -07:00 |
|
Leonardo de Moura
|
5fed774461
|
chore: HasRepr ==> Repr
|
2020-10-27 16:15:10 -07:00 |
|
Leonardo de Moura
|
10c32fcf94
|
chore: HasToString => ToString
|
2020-10-27 16:11:48 -07:00 |
|
Leonardo de Moura
|
13c2a8ff51
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Leonardo de Moura
|
78c05e8f46
|
chore: move to new frontend
|
2020-10-23 16:13:55 -07:00 |
|
Leonardo de Moura
|
7030dc91f2
|
chore: move to new frontend
|
2020-10-23 12:50:03 -07:00 |
|
Leonardo de Moura
|
5a40d9eb13
|
feat: add Subarray
|
2020-10-09 16:06:24 -07:00 |
|
Leonardo de Moura
|
749e2063cf
|
feat: add interpolated string for toString
|
2020-10-09 14:38:24 -07:00 |
|
Leonardo de Moura
|
98f7e9b3e4
|
chore: naming convention
|
2020-09-24 19:22:24 -07:00 |
|
Leonardo de Moura
|
c46e64b089
|
feat: add Array.zipWith and Array.zip
|
2020-09-23 18:24:56 -07:00 |
|
Leonardo de Moura
|
ea2e86afba
|
feat: add Array.allDiff
|
2020-09-08 16:16:14 -07:00 |
|
Leonardo de Moura
|
fc1e4cb533
|
feat: add Array.isPrefixOf
|
2020-09-08 14:40:43 -07:00 |
|
Leonardo de Moura
|
3ae3c51a8c
|
feat: add Array.partition
|
2020-09-05 08:48:15 -07:00 |
|
Leonardo de Moura
|
0199e93079
|
chore: add Array.erase
|
2020-09-04 13:35:01 -07:00 |
|
Leonardo de Moura
|
3dbd2b728b
|
feat: add Array.getMax?
|
2020-09-04 10:40:34 -07:00 |
|
Leonardo de Moura
|
47ff4d0e8e
|
chore: add helper functions
TODO: we should `Subarray` and functions/methods for it. Then, we can delete
functions such as `foldlFromM`
|
2020-08-27 14:58:27 -07:00 |
|
Leonardo de Moura
|
bd8e2d305f
|
feat: add Array.filterMap
|
2020-08-14 10:50:48 -07:00 |
|
Leonardo de Moura
|
81ae6a734b
|
feat: mark List.toArray with [matchPattern]
|
2020-08-13 14:25:47 -07:00 |
|
Leonardo de Moura
|
aefc9a473f
|
feat: add auxiliary definitions for compiling array literals in pattern matching expressions
|
2020-08-07 09:23:33 -07:00 |
|
Sebastian Ullrich
|
8f67db0101
|
refactor: never implicitly ignore monadic results
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
|
2020-04-23 11:09:59 -07:00 |
|
Sebastian Ullrich
|
f66039f7f0
|
feat: generalize Array function universes
|
2020-04-06 13:48:09 -07:00 |
|
Leonardo de Moura
|
2d7ec0b49c
|
fix: bug at unsafe umapMAux implementation
closes #125
|
2020-03-14 13:41:14 -07:00 |
|
Leonardo de Moura
|
6ad0c2cc18
|
feat: simplify unsafeCast
|
2020-03-14 13:10:56 -07:00 |
|
Leonardo de Moura
|
a0090b378b
|
feat: move Array extensionality theorems to Init
|
2020-03-13 06:39:13 -07:00 |
|
Leonardo de Moura
|
a8c3322ac8
|
doc: expand dependent pattern matching support for array literals
|
2020-03-13 06:39:13 -07:00 |
|
Leonardo de Moura
|
50acb88727
|
feat: add auxiliary function for matching array literals
|
2020-03-11 11:57:01 -07:00 |
|
Leonardo de Moura
|
36096abec0
|
feat: add Array.findIdxM? and Array.getIdx?
|
2020-02-19 14:54:55 -08:00 |
|
Leonardo de Moura
|
4427d4468b
|
feat: add modifyOp
|
2020-02-02 17:30:56 -08:00 |
|
Leonardo de Moura
|
8525584a78
|
refactor: naming consistency ensure List and Array have similar find* methods
`find?` -> takes predicate
`findSome?` -> takes a function (A -> Option B)
|
2020-01-26 15:13:05 -08:00 |
|
Leonardo de Moura
|
0d25c5f55c
|
feat: add Array.filterM
|
2020-01-19 15:18:01 -08:00 |
|
Leonardo de Moura
|
98d9022321
|
chore: cleanup and new test
|
2020-01-17 18:07:58 -08:00 |
|
Leonardo de Moura
|
7fd55477b2
|
feat: add sortDeclLevelParams
|
2020-01-05 14:35:14 -08:00 |
|
Leonardo de Moura
|
16cb6fe759
|
feat: add foldrRangeM
|
2019-12-30 08:11:23 -08:00 |
|
Leonardo de Moura
|
d2d6e85719
|
feat: add forRevM
|
2019-12-19 17:24:29 -08:00 |
|
Leonardo de Moura
|
757419ffa9
|
feat: rename fold functions initial value parameter to init
|
2019-12-19 14:44:51 -08:00 |
|
Leonardo de Moura
|
f334e7e89c
|
chore: cleanup and remove Array.getA
|
2019-12-19 07:09:51 -08:00 |
|