Commit graph

19 commits

Author SHA1 Message Date
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
Leonardo de Moura
d9d1c67d86 feat: add cdot notation detection
We need `fun` elaboration.
2019-12-17 10:21:39 -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
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
013bc5b589 feat: add modifyM 2019-11-23 07:37:33 -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
Renamed from library/Init/Data/Array/Basic.lean (Browse further)