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
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
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
e97df2f61b
feat: functions to unfold at simp
2021-02-15 15:32:25 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
7bdd3ae5a2
feat: simplify ctor_1 ... = ctor_2 ...
2021-02-15 12:40:19 -08:00
Leonardo de Moura
0787886cea
feat: improve simp local lemma elaboration
2021-02-13 18:55:19 -08:00
Leonardo de Moura
2944da2a0b
feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules
2021-02-13 18:55:19 -08:00
Leonardo de Moura
3a9cd7e85b
refactor: use Simp.Context instead of Config+SimpLemmas+CongrLemmas
2021-02-13 18:55:19 -08:00
Leonardo de Moura
4ac78266ad
fix: make sure temporary metavars don't leak
2021-02-12 16:52:56 -08:00
