Leonardo de Moura
9b0dfc4b90
feat: convert "orphan" kernel nat literals n into ofNat n
2021-09-08 14:58:13 -07:00
Leonardo de Moura
445cc3085f
refactor: avoid Name, MVarId, and FVarId confusion
2021-09-07 19:06:50 -07:00
Leonardo de Moura
7a69c6483d
feat: add congr conv tactic
2021-09-01 18:32:21 -07:00
Leonardo de Moura
5f762171cc
feat: add support for split at
2021-08-31 19:35:07 -07:00
Leonardo de Moura
6d4422e5ac
refactor: add Simp.tryLemma?
2021-08-31 12:32:34 -07:00
Leonardo de Moura
ce47000e33
fix: missing whnf at tryLemma?
2021-08-30 08:33:58 -07:00
Leonardo de Moura
e04976614f
feat: check if metavar is not assigned at simp tactics
...
and make sure `simpLocalDecl` does not change the goal if it didn't simplify
2021-08-17 21:32:32 -07:00
Leonardo de Moura
4cfbe6030f
feat: add simpLocalDecl
2021-08-17 21:32:32 -07:00
Leonardo de Moura
60ff468a8b
feat: add simpGoal helper method
...
chore: rename `simpGoal?`
2021-08-17 21:32:32 -07:00
Leonardo de Moura
5a76f70bc8
feat: add optional argument discharge? to simp basic methods
2021-08-17 21:32:32 -07:00
Leonardo de Moura
f59b9813fb
feat: add environment extension for caching Simp.Context for splitIf
2021-08-16 13:05:01 -07:00
Leonardo de Moura
ca0c205389
feat: add registerSimpAttr
2021-08-16 09:59:58 -07:00
Leonardo de Moura
3c68703f39
feat: elaborate <- modifier at simp arguments
2021-08-15 07:07:58 -07:00
Leonardo de Moura
a821dcbff2
chore: enforce naming convention for theorems
...
see issue #402
fix: `ElabTerm.lean`
2021-08-07 12:48:38 -07:00
Wojciech Nawrocki
f51b80060d
feat: generic tagged Format
2021-08-01 09:58:44 +02:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Leonardo de Moura
edb203ca54
fix: fixes #481
2021-05-21 20:40:26 -07:00
Leonardo de Moura
795e3a8646
chore: use "theorem" instead of "lemma" in messages
2021-05-21 20:35:23 -07:00
Leonardo de Moura
62ee8cfcea
feat: add MonadBacktrack instance for SimpM
2021-05-16 12:49:33 -07:00
Leonardo de Moura
ac90052139
feat: add option for controlling how deep we go when trying to discharge simp theorem hypotheses
2021-05-16 12:32:05 -07:00
Leonardo de Moura
f850820029
feat: add mkInjectiveTheorems
2021-05-13 22:09:50 -07:00
Leonardo de Moura
6dbf227cf2
fix: issues #387 part 2
...
see #387
2021-04-10 15:51:07 -07:00
Leonardo de Moura
91cb4aad2a
refactor: simplify and document SimpLemma encoding
2021-04-10 15:03:04 -07:00
Leonardo de Moura
4f09390b8e
feat: create SimpLemmas.Proof.abst at the simp tactic frontend
2021-04-10 14:17:43 -07:00
Leonardo de Moura
8be9a13679
feat: support for SimpLemma.Proof.abst
2021-04-10 12:46:48 -07:00
Leonardo de Moura
a1205afac2
feat: allow simp lemmas to be AbstractMvarsResult
2021-04-10 11:37:39 -07:00
Leonardo de Moura
566fad77d4
chore: helper methods
2021-03-27 18:48:03 -07:00
Leonardo de Moura
ce1dda8eea
fix: missing withMVarContext
2021-03-24 18:25:41 -07:00
Sebastian Ullrich
2f168e3364
feat: mkConstWithLevelParams
2021-03-20 08:28:18 -07:00
Leonardo de Moura
86a204d8a1
feat: add simp_all tactic
...
cc @Kha
2021-03-19 22:34:35 -07:00
Leonardo de Moura
d70740fef2
fix: location notation and simp
2021-03-19 19:54:22 -07:00
Leonardo de Moura
94465e8a02
feat: add helper simp methods
2021-03-19 14:11:15 -07:00
Leonardo de Moura
dd8ead186f
feat: allow caller to set lemma id
2021-03-18 14:25:16 -07:00
Leonardo de Moura
1af02dcaca
feat: allow users to mark definitions with [simp]
...
cc @JasonGross @Kha
2021-03-17 19:11:55 -07:00
Leonardo de Moura
3208faa192
feat: add set of declarations to unfold at SimpLemmas
2021-03-17 18:52:23 -07:00
Leonardo de Moura
89797c4485
chore: improve congrDefault
...
We don't need `congrMatch` anymore.
2021-03-16 15:59:11 -07:00
Leonardo de Moura
8227d3afcd
feat: support for simplifying match discriminants
2021-03-16 15:51:36 -07:00
Leonardo de Moura
bf8119a5cd
chore: convert keywords to snake_case
...
Again `!` is only for functions that can panic.
2021-03-12 13:34:51 -08:00
Leonardo de Moura
be841a7cad
chore: throwError! => throwError, throwErrorAt! => throwErrorAt
...
@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
2021-03-11 11:59:45 -08:00
Leonardo de Moura
68143ca8ba
chore: trace[...]! ==> trace[...]
...
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
2021-03-10 18:44:43 -08:00
Leonardo de Moura
8f580a5a70
refactor: remove SimpLemmaKind
2021-03-09 19:25:02 -08:00
Leonardo de Moura
0ea267e4de
feat: add simp lemma preprocessor
2021-03-09 19:16:14 -08:00
Leonardo de Moura
66f1a88f2c
feat: simp [-decl]
2021-03-04 17:50:44 -08:00
Leonardo de Moura
db499a646f
chore: add profileitM for simp
2021-03-04 17:27:01 -08:00
Leonardo de Moura
fe94731779
perf: do not use decide for rewriting True/False
2021-03-04 13:50:17 -08:00
Leonardo de Moura
9baee4354c
chore: add trace.Debug.Meta.Tactic.simp
...
It is an attempt to distinguish trace messages that are relevant only
for developers.
@Kha I am considering using the prefix `trace.Debug` for (debugging) messages that
are just for us.
2021-03-04 12:27:10 -08:00
Leonardo de Moura
960e964b71
feat: allow user to "erase" [simp] lemmas
2021-03-04 11:36:12 -08:00
Leonardo de Moura
152a84c468
perf: reject rewrites that produce same expr
2021-03-03 20:20:22 -08: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
