Leonardo de Moura
|
d8ca6d847b
|
test: lost synthetic mvar issue
|
2021-02-20 13:01:36 -08:00 |
|
Leonardo de Moura
|
2cf56f5e10
|
fix: synthesizeSyntheticMVars at liftTacticElabM
|
2021-02-20 13:00:26 -08:00 |
|
Leonardo de Moura
|
65ea26422a
|
fix: use Term.withSynthesize at rewrite
|
2021-02-20 12:59:41 -08:00 |
|
Leonardo de Moura
|
bcd8f09672
|
feat: monad polymorphic withSynthesize
|
2021-02-20 12:32:05 -08:00 |
|
Leonardo de Moura
|
8fa1ecde49
|
fix: throw error when default value contains metavariables
|
2021-02-20 11:31:56 -08:00 |
|
Leonardo de Moura
|
caf54d78e2
|
feat: add Control/Lawful.lean
|
2021-02-20 09:37:43 -08:00 |
|
Leonardo de Moura
|
6eeccdd675
|
test: for field auto implicit bound feature
|
2021-02-20 07:52:42 -08:00 |
|
Leonardo de Moura
|
62221f8a60
|
chore: update stage0
|
2021-02-20 07:51:30 -08:00 |
|
Leonardo de Moura
|
a264268a63
|
fix: structure field auto bound implicits
|
2021-02-20 07:46:55 -08:00 |
|
Sebastian Ullrich
|
0ac95965dc
|
chore: update vscode-lean4
|
2021-02-20 14:16:47 +01:00 |
|
Leonardo de Moura
|
0c4be69b5e
|
chore: update stage0
|
2021-02-19 15:24:33 -08:00 |
|
Leonardo de Moura
|
2264d2e99a
|
chore: update stage0
|
2021-02-19 15:19:07 -08:00 |
|
Leonardo de Moura
|
e1f6965266
|
feat: allow user to define rewrite lemmas with (local) match expressions
|
2021-02-19 15:18:19 -08:00 |
|
Leonardo de Moura
|
c55c8ee01b
|
chore: update stage0
|
2021-02-19 13:53:08 -08:00 |
|
Leonardo de Moura
|
d493e700cc
|
fix: matchUnit simplification
|
2021-02-19 13:51:08 -08:00 |
|
Leonardo de Moura
|
d1d26e5ba6
|
fix: use try clear
|
2021-02-19 13:46:02 -08:00 |
|
Leonardo de Moura
|
2861f71c61
|
feat: add option autoLift
|
2021-02-19 11:02:58 -08:00 |
|
Leonardo de Moura
|
c06ca8304d
|
fix: test
|
2021-02-18 16:54:45 -08:00 |
|
Leonardo de Moura
|
0a280793c7
|
chore: update stage0
|
2021-02-18 11:34:53 -08:00 |
|
Leonardo de Moura
|
8392b09db2
|
feat: shouldAddAsStar only for nested terms
|
2021-02-18 11:33:56 -08:00 |
|
Joe Hendrix
|
ffef5635bb
|
fix: Json.num
Handle negative numbers correctly.
|
2021-02-18 13:27:31 +01:00 |
|
Leonardo de Moura
|
51771d5d07
|
feat: erase _discr auxiliary variables
|
2021-02-17 18:10:02 -08:00 |
|
Leonardo de Moura
|
083efd5825
|
chore: update stage0
|
2021-02-17 17:14:40 -08:00 |
|
Leonardo de Moura
|
c5673b6025
|
feat: auxiliary tactic for erasing auxiliary discriminants
|
2021-02-17 16:59:21 -08:00 |
|
Leonardo de Moura
|
ea26caa3fa
|
chore: minor cleanup
|
2021-02-17 16:47:30 -08:00 |
|
Leonardo de Moura
|
6263141f7b
|
fix: preserve InfoTree when tactics fail
cc @Kha @Vtec234
|
2021-02-17 15:20:33 -08:00 |
|
Leonardo de Moura
|
64413e9d4a
|
chore: cleanup
|
2021-02-17 15:13:05 -08:00 |
|
Leonardo de Moura
|
e139a539f6
|
chore: update stage0
|
2021-02-17 13:56:21 -08:00 |
|
Leonardo de Moura
|
df8634e9ad
|
fix: assertAfter
|
2021-02-17 13:52:43 -08:00 |
|
Leonardo de Moura
|
bb2ca97df9
|
refactor: add options for controlling whether variables are included or not at mkLambdaFVars and mkForallFVars
|
2021-02-17 13:49:27 -08:00 |
|
Leonardo de Moura
|
c97ae92afe
|
chore: cleanup
|
2021-02-17 13:03:24 -08:00 |
|
Leonardo de Moura
|
79a4aebf96
|
feat: add byCases tactic
|
2021-02-17 13:03:24 -08:00 |
|
Leonardo de Moura
|
08927f1e66
|
test: tactic framework and AC by reflection
|
2021-02-17 13:03:24 -08:00 |
|
Sebastian Ullrich
|
187a614575
|
chore: make tryFinally a def
|
2021-02-17 12:04:20 +01:00 |
|
Sebastian Ullrich
|
c0a3ea7c7e
|
doc: theorem naming
|
2021-02-17 12:03:58 +01:00 |
|
Sebastian Ullrich
|
010338cb18
|
chore: improve "no elaborator" error message
|
2021-02-17 11:52:22 +01:00 |
|
Leonardo de Moura
|
1a7535263e
|
fix: unfolding class projections at simp
|
2021-02-16 17:55:57 -08:00 |
|
Leonardo de Moura
|
399af03c7c
|
refactor: move defeq unfolding to reduce, use transform to implement dsimp
|
2021-02-16 17:41:18 -08:00 |
|
Leonardo de Moura
|
15e6ae2cdb
|
chore: cleanup
|
2021-02-16 16:16:21 -08:00 |
|
Leonardo de Moura
|
2ef6605cdf
|
feat: do not simplify proofs
|
2021-02-16 16:13:56 -08:00 |
|
Leonardo de Moura
|
5f80659b45
|
fix: unfold constants at simp
|
2021-02-16 15:42:31 -08:00 |
|
Leonardo de Moura
|
3e65f586cc
|
fix: smart unfolding
|
2021-02-16 15:39:07 -08:00 |
|
Leonardo de Moura
|
5e24da0c2e
|
fix: simp argument issue
See new test.
|
2021-02-16 13:12:57 -08:00 |
|
Leonardo de Moura
|
d1009e8405
|
chore: add simp lemmas, theorem naming convention
|
2021-02-16 11:53:49 -08:00 |
|
Leonardo de Moura
|
186c620f59
|
chore: update stage0
|
2021-02-16 10:47:15 -08:00 |
|
Leonardo de Moura
|
504a015f9b
|
fix: borrowing annotations
|
2021-02-16 10:30:30 -08:00 |
|
Sebastian Ullrich
|
e8812ed834
|
fix: memory leak at Nat.ble
|
2021-02-16 14:24:28 +01:00 |
|
Sebastian Ullrich
|
1490d095a8
|
fix: delaborator: bind without lambda
|
2021-02-16 12:07:46 +01:00 |
|
Leonardo de Moura
|
4ec85a39a5
|
fix: Not should not be reducible, special support for Ne
Unification hint for `Not`
|
2021-02-15 17:36:11 -08:00 |
|
Leonardo de Moura
|
242a8dcfbf
|
test: simp
|
2021-02-15 17:09:51 -08:00 |
|