max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
19777 commits 1 branch 0 tags 5.3 GiB
Commit graph

70 commits

Author SHA1 Message Date
Leonardo de Moura
b8ea55c989 feat: expose some transcendental functions from the C library 
cc @dselsam
 2020-04-06 15:22:25 -07:00
Leonardo de Moura
705530b62b fix: remove DecidableEq for Float 
We cannot implement `DecidableEq Float` using C equality for
`double`. Reason: the C implementation is not even reflexive.
If we need `DecidableEq Float`, we will need to provide our own
implementation (i.e., a wrapper around the one provided by the
hardware). In this commit, we implement `HasBeq Float` instead.

cc @dselsam
 2020-04-06 14:10:18 -07:00
Sebastian Ullrich
f66039f7f0 feat: generalize Array function universes 2020-04-06 13:48:09 -07:00
Leonardo de Moura
485034bbba fix: bug at ir.cpp 2020-04-03 17:39:28 -07:00
Leonardo de Moura
c236a179f2 feat: enable externs 2020-04-03 17:19:48 -07:00
Leonardo de Moura
0e2ebd36ff feat: make sure Float is in WHNF 2020-04-03 17:07:29 -07:00
Leonardo de Moura
71397aad36 feat: runtime primitives 2020-04-03 15:55:39 -07:00
Leonardo de Moura
52cffcb67f feat: add Float.lean 2020-04-03 15:40:38 -07:00
Sebastian Ullrich
b6fc9428f1 fix: support Windows newlines and '\r' escape 2020-03-27 13:21:21 -07:00
Leonardo de Moura
2c12a073fa fix: missing file 2020-03-23 15:49:22 -07:00
Leonardo de Moura
12c5075c67 fix: String.dropRight 2020-03-23 14:51:05 -07:00
Leonardo de Moura
41949ee801 refactor: String.toNat ==> String.toNat? and String.toNat! 2020-03-23 14:29:48 -07:00
Sebastian Ullrich
ed14375dad feat: sort and deduplicate "expected" tokens in parser error messages 2020-03-19 17:17:08 -07:00
Sebastian Ullrich
e999fa678d feat: add some useful helper functions I didn't actually use in the end 2020-03-19 17:14:31 -07:00
Leonardo de Moura
cd8bd55311 feat: make sure Char.ofNat can be efficiently reduced in the kernel and WHNF 2020-03-18 16:41:48 -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
0893b62598 perf: avoid unnecessary overhead at HashSet 
List instead of AssocList saves one word per entry.
 2020-03-02 08:40:15 -08:00
Leonardo de Moura
58ddeedced feat: add List.replace 2020-03-02 08:30:20 -08:00
Leonardo de Moura
0781c74754 chore: variable order consistency 2020-02-24 18:29:24 -08:00
Leonardo de Moura
370dada9a3 feat: add findEntry? functions 2020-02-24 15:47:59 -08:00
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