Leonardo de Moura
|
36096abec0
|
feat: add Array.findIdxM? and Array.getIdx?
|
2020-02-19 14:54:55 -08:00 |
|
Leonardo de Moura
|
ca20bb112f
|
feat: add helper
|
2020-02-17 12:10:52 -08:00 |
|
Leonardo de Moura
|
3c235c3613
|
chore: naming convention
|
2020-02-09 17:10:20 -08:00 |
|
Leonardo de Moura
|
3f4c27efa5
|
feat: add getFieldViews
|
2020-02-05 19:15:05 -08:00 |
|
Leonardo de Moura
|
bcfaeaceab
|
feat: change ite and dite argument order
Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
|
2020-02-03 14:11:29 -08:00 |
|
Leonardo de Moura
|
4427d4468b
|
feat: add modifyOp
|
2020-02-02 17:30:56 -08:00 |
|
Leonardo de Moura
|
6a046a11c2
|
chore: remove coeSortBool
It is interacting with new `Coe`.
We can add it back at `Coe.lean` after we remove `HasCoe.lean`
|
2020-01-28 19:07:02 -08:00 |
|
Leonardo de Moura
|
e9e4dfe1ff
|
feat: add new Coe.lean
|
2020-01-28 13:10:30 -08:00 |
|
Leonardo de Moura
|
7809274c3a
|
chore: Coe.lean ==> HasCoe.lean
|
2020-01-28 08:55:22 -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
|
364bb7bdf7
|
fix: proper Name literals
cc @kha
|
2020-01-24 12:38:15 -08:00 |
|
Leonardo de Moura
|
67fb63c9fd
|
feat: use mpz_pow_ui to implement Nat.pow
|
2020-01-21 09:16:38 -08:00 |
|
Leonardo de Moura
|
0d25c5f55c
|
feat: add Array.filterM
|
2020-01-19 15:18:01 -08:00 |
|
Leonardo de Moura
|
1bc14d1c62
|
feat: add List.findM?
|
2020-01-18 17:42:10 -08:00 |
|
Leonardo de Moura
|
98d9022321
|
chore: cleanup and new test
|
2020-01-17 18:07:58 -08:00 |
|
Simon Hudon
|
6d8927da10
|
fix: little details
|
2020-01-12 08:02:48 -08:00 |
|
Simon Hudon
|
92c8773137
|
feat: file IO using handles
|
2020-01-12 08:02:48 -08:00 |
|
Leonardo de Moura
|
7fd55477b2
|
feat: add sortDeclLevelParams
|
2020-01-05 14:35:14 -08:00 |
|
Leonardo de Moura
|
b429794ebc
|
chore: naming convention
|
2020-01-01 15:04:20 -08:00 |
|
Sebastian Ullrich
|
81381d5c77
|
feat: make all antiquotation kinds optional
|
2019-12-30 08:24:29 -08:00 |
|
Leonardo de Moura
|
16cb6fe759
|
feat: add foldrRangeM
|
2019-12-30 08:11:23 -08:00 |
|
Sebastian Ullrich
|
3b37737c8a
|
fix: leaks
|
2019-12-22 15:09:19 -08:00 |
|
Leonardo de Moura
|
d53c5a31cb
|
refactor: use PersistentArray to implement MessageLog
Motivation: consistency. Now, Traces and MessageLog use the same datastructure.
|
2019-12-22 08:11:20 -08:00 |
|
Leonardo de Moura
|
050008cb84
|
refactor: use PersistentArray instead of Array for default [MonadTracer] implementation
Motivation: flexibility. Now, the default implementation is better
suited for code that uses traces nonlinearly (e.g., `TermElabM`).
|
2019-12-22 07:36:26 -08:00 |
|
Leonardo de Moura
|
c14192670f
|
feat: add PersistentHashMap.forM
|
2019-12-21 09:22:10 -08:00 |
|
Leonardo de Moura
|
d2d6e85719
|
feat: add forRevM
|
2019-12-19 17:24:29 -08:00 |
|
Leonardo de Moura
|
40f7caca0b
|
feat: add tailrec filterM and filterRevM
|
2019-12-19 15:06:16 -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 |
|
Sebastian Ullrich
|
e8944fcf9d
|
feat: implement match_syntax
|
2019-12-17 12:16:34 -08:00 |
|
Leonardo de Moura
|
d9d1c67d86
|
feat: add cdot notation detection
We need `fun` elaboration.
|
2019-12-17 10:21:39 -08:00 |
|
Leonardo de Moura
|
b8257f2317
|
feat: add HasOfNat
It is used to encode numerical literals in the new frontend.
|
2019-12-16 10:28:28 -08:00 |
|
Leonardo de Moura
|
067dca5a65
|
chore: naming convention
|
2019-12-15 18:28:00 -08:00 |
|
Leonardo de Moura
|
d551ff653d
|
feat: add getOp for a[i] notation
|
2019-12-15 17:52:03 -08:00 |
|
Leonardo de Moura
|
a80c5c8339
|
chore: naming convention
|
2019-12-14 12:00:25 -08:00 |
|
Leonardo de Moura
|
8fd70ee882
|
feat: add builtin notation
|
2019-12-11 16:22:23 -08:00 |
|
Leonardo de Moura
|
6cd7d568d3
|
chore: HasModn ==> HasModN
|
2019-12-11 15:36:58 -08:00 |
|
Leonardo de Moura
|
c3005671f5
|
chore: avoid ^do ...
|
2019-12-11 06:19:12 -08:00 |
|
Leonardo de Moura
|
43d7ae3938
|
fix: missing annotation
|
2019-12-02 10:42:50 -08:00 |
|
Leonardo de Moura
|
e8bd90a753
|
fix: performance issue introduced by 2809cea147
|
2019-11-27 05:43:28 -08:00 |
|
Leonardo de Moura
|
2809cea147
|
chore: remove DecidableEq workaround
We have better indexing now.
|
2019-11-26 17:30:18 -08:00 |
|
Leonardo de Moura
|
c6048f0f94
|
feat: generalize binInsert
|
2019-11-23 08:20:20 -08:00 |
|
Leonardo de Moura
|
013bc5b589
|
feat: add modifyM
|
2019-11-23 07:37:33 -08:00 |
|
Leonardo de Moura
|
2e610227e4
|
feat: add Array.binInsert
|
2019-11-22 18:22:26 -08:00 |
|
Leonardo de Moura
|
69723b48c3
|
feat: add Array.insertAt
|
2019-11-22 17:42:27 -08:00 |
|
Leonardo de Moura
|
c445199747
|
chore: library/Init ==> src/Init
cc @Kha @dselsam @cipher1024
|
2019-11-22 06:06:05 -08:00 |
|