Leonardo de Moura
|
49e33fdb23
|
chore: fix tests
|
2022-03-15 11:35:47 -07:00 |
|
Leonardo de Moura
|
e1ba83d902
|
chore: update stage0
|
2022-03-15 11:31:39 -07:00 |
|
Leonardo de Moura
|
d3e2dfb079
|
perf: optimize mkApp
|
2022-03-15 11:31:15 -07:00 |
|
Leonardo de Moura
|
9d73317d76
|
perf: faster Expr.data
|
2022-03-15 11:30:41 -07:00 |
|
Leonardo de Moura
|
d2dc38fdb6
|
perf: use HasConstCache to minimize the number of visited terms at Structural and WF
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2022-03-15 08:40:47 -07:00 |
|
Leonardo de Moura
|
5283007aa4
|
feat: add HasConstCache
|
2022-03-15 08:39:48 -07:00 |
|
Leonardo de Moura
|
3278d7bc2a
|
chore: update stage0
|
2022-03-15 07:16:17 -07:00 |
|
Leonardo de Moura
|
ca6453a0ab
|
perf: efficient unsigned hash(expr const & e)
|
2022-03-15 07:15:00 -07:00 |
|
Leonardo de Moura
|
eccd5c11c9
|
perf: removeUnusedEqnHypotheses
|
2022-03-15 06:53:43 -07:00 |
|
Leonardo de Moura
|
2b71bc84f3
|
perf: try injection before contradiction at mkSplitterProof
|
2022-03-15 05:37:10 -07:00 |
|
Leonardo de Moura
|
c3c0b8b8a2
|
chore: remove unnecessary code
|
2022-03-15 05:26:33 -07:00 |
|
Leonardo de Moura
|
aa68057c85
|
chore: more general type universes in example
|
2022-03-15 05:19:02 -07:00 |
|
Leonardo de Moura
|
7ee7ca30b8
|
fix: index out of bounds
|
2022-03-15 05:16:19 -07:00 |
|
Leonardo de Moura
|
4e261b15e5
|
fix: smart unfolding bug in over applications
|
2022-03-14 19:17:21 -07:00 |
|
Leonardo de Moura
|
eb7539ef77
|
fix: mkEqnTypes overapplied lhs in equational theorems
This issue was exposed by the "Dependent de Bruijn indices" from CPDT.
|
2022-03-14 17:42:21 -07:00 |
|
Leonardo de Moura
|
c6dae18787
|
chore: add helper theorems
|
2022-03-14 16:24:05 -07:00 |
|
Leonardo de Moura
|
40f608bfbd
|
chore: cleanup String.extract reference implementation
|
2022-03-14 16:23:13 -07:00 |
|
Leonardo de Moura
|
8e29747fe7
|
feat: add simp theorem (a : Nat) : (a ≤ 0) = (a = 0)
|
2022-03-14 15:43:42 -07:00 |
|
Leonardo de Moura
|
bbe6bd4e72
|
chore: simplify String.utf8ByteSize reference implementation
|
2022-03-14 15:42:58 -07:00 |
|
Leonardo de Moura
|
14ed473777
|
feat: mark Nat.zero_le as simp theorem
|
2022-03-14 15:19:52 -07:00 |
|
Leonardo de Moura
|
7fda1f47f8
|
test: add test for issue fixed in previous commit
|
2022-03-14 14:11:08 -07:00 |
|
Leonardo de Moura
|
86fc089e07
|
fix: tryAutoCongrTheorem? may still use dsimp for fixed arguments
Reviewed-by: Leonardo de Moura <leonardo@microsoft.com>
|
2022-03-14 14:04:28 -07:00 |
|
Leonardo de Moura
|
ef154ec0cf
|
test: add TreeNode example using for in notation
|
2022-03-14 11:52:54 -07:00 |
|
Leonardo de Moura
|
cab3217b05
|
feat: add forIn'_eq_forIn theorem for lists
|
2022-03-14 11:50:47 -07:00 |
|
Leonardo de Moura
|
2ac9cfb7b1
|
fix: eta expand partial applications of recursive function being defined
|
2022-03-14 10:05:33 -07:00 |
|
Leonardo de Moura
|
801552e1ac
|
chore: fix tests
|
2022-03-14 10:05:33 -07:00 |
|
Leonardo de Moura
|
9988faf8bd
|
fix: missing mkRecAppWithSyntax
|
2022-03-14 10:05:33 -07:00 |
|
Leonardo de Moura
|
02145f66cf
|
chore: fix typo
|
2022-03-14 10:05:33 -07:00 |
|
Sebastian Ullrich
|
147a5c2933
|
chore: prefer LEAN_SRC_PATH
|
2022-03-14 17:24:25 +01:00 |
|
Leonardo de Moura
|
d2cc5b4a83
|
chore: fix test
|
2022-03-13 15:53:21 -07:00 |
|
Leonardo de Moura
|
fa0964c07e
|
fix: preserve variable name at WF decreasing goals when function has only one non fixed argument
|
2022-03-13 13:20:07 -07:00 |
|
Leonardo de Moura
|
060be7e7ec
|
fix: :: is infix right
|
2022-03-13 09:25:56 -07:00 |
|
Leonardo de Moura
|
672a889c83
|
test: add hlist pattern match example
|
2022-03-13 09:15:55 -07:00 |
|
Leonardo de Moura
|
30c153aa76
|
chore: update stage0
|
2022-03-12 20:18:20 -08:00 |
|
Leonardo de Moura
|
bfe57a1cb0
|
chore: simplify definition
|
2022-03-12 20:16:45 -08:00 |
|
Leonardo de Moura
|
231120c118
|
chore: update RELEASES.md
|
2022-03-12 20:02:39 -08:00 |
|
Leonardo de Moura
|
5707cab7bf
|
feat: improve #eval command
Now, if it fails to synthesize the TC instance, it applies `whnf` and
tries again.
|
2022-03-12 19:55:15 -08:00 |
|
Leonardo de Moura
|
3cd41acd14
|
test: HList with notation overloads
|
2022-03-12 19:47:57 -08:00 |
|
Leonardo de Moura
|
af5a24140a
|
test: simple type checker at CPDT
|
2022-03-12 18:44:52 -08:00 |
|
Leonardo de Moura
|
7e3519a3a2
|
test: add CPDT first example
|
2022-03-12 17:06:20 -08:00 |
|
Leonardo de Moura
|
f0c31d7e28
|
feat: allow rw to unfold nonrecursive definitions too
|
2022-03-12 15:44:52 -08:00 |
|
Leonardo de Moura
|
c0a72172f1
|
chore: update stage0
|
2022-03-12 15:35:09 -08:00 |
|
Leonardo de Moura
|
7af09ac009
|
refactor: move equation theorem cache to Meta/Eqns.lean
|
2022-03-12 15:34:32 -08:00 |
|
Leonardo de Moura
|
cf0ca026fb
|
feat: equation theorems at rw
|
2022-03-12 13:53:02 -08:00 |
|
Leonardo de Moura
|
9d1dbada79
|
feat: only try to generate equation theorems for definitions whose types are not propositions
|
2022-03-12 13:44:33 -08:00 |
|
Leonardo de Moura
|
8a46668884
|
chore: update stage0
|
2022-03-12 10:46:17 -08:00 |
|
Leonardo de Moura
|
a6bfefe5bd
|
fix: nasty performance problem at isDefEq
This problem was originally exposed by the `Array.eraseIdxAux`.
|
2022-03-12 10:44:43 -08:00 |
|
Leonardo de Moura
|
eddcedb58c
|
fix: pattern normalization code
|
2022-03-12 06:07:04 -08:00 |
|
Lars
|
95cf18457d
|
chore: address review comments
|
2022-03-12 13:25:35 +00:00 |
|
Sebastian Ullrich
|
82c682d385
|
chore: remove redundant proof
|
2022-03-12 11:12:56 +01:00 |
|