Leonardo de Moura
|
1fd3cfb19f
|
feat: pretty print let_fun
|
2021-09-11 05:15:11 -07:00 |
|
Leonardo de Moura
|
f26c905130
|
refactor: split Structural.lean into smaller files
|
2021-09-11 03:40:51 -07:00 |
|
Leonardo de Moura
|
964095ba6e
|
chore: clean up before refactoring
|
2021-09-11 02:58:55 -07:00 |
|
Leonardo de Moura
|
c06ae66c53
|
feat: add withScope
|
2021-09-10 19:20:25 -07:00 |
|
Leonardo de Moura
|
5154f462f8
|
feat: add reduce conv tactic
|
2021-09-09 17:47:10 -07:00 |
|
Leonardo de Moura
|
496cc92ae9
|
feat: add simpMatch helper conv tactic
|
2021-09-09 17:29:32 -07:00 |
|
Leonardo de Moura
|
5a7badd69a
|
feat: add support for erasing keyed attributes
This commit addresses any issue described at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Eq.2Endrec.20vs.20Eq.2Erec
|
2021-09-09 14:28:41 -07:00 |
|
Leonardo de Moura
|
b5b5370181
|
feat: add delta to conv mode
|
2021-09-09 13:07:33 -07:00 |
|
Leonardo de Moura
|
4087525cba
|
feat: add delta tactic
|
2021-09-09 13:07:33 -07:00 |
|
Leonardo de Moura
|
cd75132378
|
refactor: add withLocation combinator
|
2021-09-09 13:07:33 -07:00 |
|
Leonardo de Moura
|
474395aae4
|
perf: use binary search
|
2021-09-08 16:54:54 -07:00 |
|
Leonardo de Moura
|
193d4dc9f5
|
feat: optimized deriving DecidableEq for enumeration types
The proof term is liner on the number of constructors, but type
checking is not linear because the reduction engine in the kernel is
not efficient.
|
2021-09-08 16:21:32 -07:00 |
|
Christian Pehle
|
bd02f16b43
|
feat: optimized ``deriving BEq`` for enumeration types
|
2021-09-08 14:57:21 -07:00 |
|
Leonardo de Moura
|
12af1480d6
|
feat: add specialize tactic
|
2021-09-08 08:00:02 -07:00 |
|
Leonardo de Moura
|
445cc3085f
|
refactor: avoid Name, MVarId, and FVarId confusion
|
2021-09-07 19:06:50 -07:00 |
|
Leonardo de Moura
|
3714cf16ec
|
refactor: lazy evaluation for <|>
see #617
|
2021-09-07 17:06:10 -07:00 |
|
Leonardo de Moura
|
55f01fb6e1
|
feat: elaborate binop_lazy%
|
2021-09-07 13:30:09 -07:00 |
|
Leonardo de Moura
|
5a862a06c6
|
chore: remove leftover
|
2021-09-07 12:57:27 -07:00 |
|
Leonardo de Moura
|
f46eedac84
|
fix: fixes #655
|
2021-09-07 12:17:28 -07:00 |
|
Leonardo de Moura
|
d43a1c7d9a
|
chore: move Constructions to Meta
|
2021-09-06 10:51:11 -07:00 |
|
Leonardo de Moura
|
a8044eb252
|
feat: improve Match module for patterns containing Fin and UInt literals
|
2021-09-05 20:43:40 -07:00 |
|
Leonardo de Moura
|
c3bb948009
|
feat: ignore nested proofs in patterns
|
2021-09-05 15:46:03 -07:00 |
|
Leonardo de Moura
|
029c5b74a2
|
feat: ignore implicit arguments at congr conv tactic
|
2021-09-05 09:44:52 -07:00 |
|
Leonardo de Moura
|
d3c487ddbf
|
feat: change lhs and rhs conv tactic semantics
They can now be applied to non binary applications.
|
2021-09-05 09:29:40 -07:00 |
|
Leonardo de Moura
|
aedc706e7d
|
feat: in modifier at conv tactic
It is just a macro for `pattern`
|
2021-09-04 18:20:33 -07:00 |
|
Leonardo de Moura
|
41cfef5bc4
|
feat: add pattern conv tactic
|
2021-09-04 18:02:46 -07:00 |
|
Leonardo de Moura
|
53a3831fd5
|
feat: add apply conv macro
|
2021-09-03 20:23:15 -07:00 |
|
Leonardo de Moura
|
94bc386fb4
|
feat: remark goals as conv goals at the end of nested tactic block
|
2021-09-03 19:52:51 -07:00 |
|
Leonardo de Moura
|
de455a9010
|
chore: add tactic' => ... which preserves the conv goal annotation
|
2021-09-03 19:41:39 -07:00 |
|
Leonardo de Moura
|
6988560177
|
feat: apply allGoals (try rfl) at end of conv nested blocks
|
2021-09-03 19:21:34 -07:00 |
|
Leonardo de Moura
|
e6c9da0fcc
|
feat: add support for implication at congr conv tactic
|
2021-09-03 18:50:19 -07:00 |
|
Leonardo de Moura
|
69075c775f
|
fix: missing withMainContext
|
2021-09-03 16:57:24 -07:00 |
|
Leonardo de Moura
|
44e7033c27
|
feat: add support for forall_congr at conv
|
2021-09-03 16:57:15 -07:00 |
|
Leonardo de Moura
|
3f70bc543f
|
feat: add simp conv tactic
|
2021-09-03 12:06:29 -07:00 |
|
Leonardo de Moura
|
75b8d9aa86
|
feat: add support for classes with a prefix of outParams at deriving ...
|
2021-09-03 11:33:09 -07:00 |
|
Leonardo de Moura
|
bbb74bfd9a
|
feat: elaborate optional deriving after def
|
2021-09-03 10:22:17 -07:00 |
|
Leonardo de Moura
|
d682d60025
|
chore: cleanup
|
2021-09-03 09:48:36 -07:00 |
|
Leonardo de Moura
|
35c0cc3c91
|
feat: deriving support for type aliases
|
2021-09-03 09:33:01 -07:00 |
|
Leonardo de Moura
|
8a249bddd2
|
feat: add try rfl at end of convTarget
|
2021-09-03 08:14:47 -07:00 |
|
Leonardo de Moura
|
b5b5ef6fdf
|
feat: add funext conv tactic
|
2021-09-03 08:00:37 -07:00 |
|
Leonardo de Moura
|
95b83ac2c0
|
feat: add 'conv at .. => ..' support
|
2021-09-02 19:40:08 -07:00 |
|
Leonardo de Moura
|
7b8ee8f9d8
|
feat: add 'change' conv tactic
|
2021-09-02 19:26:25 -07:00 |
|
Leonardo de Moura
|
397774157f
|
feat: nested tactic support in conv mode
|
2021-09-02 19:12:05 -07:00 |
|
Leonardo de Moura
|
39adda8ffe
|
fix: missing goals
|
2021-09-02 19:11:52 -07:00 |
|
Leonardo de Moura
|
41ce24e2c6
|
feat: add done and traceState conv tactics
|
2021-09-02 18:46:03 -07:00 |
|
Leonardo de Moura
|
33361929b9
|
feat: add rewrite conv tactic
|
2021-09-02 18:13:19 -07:00 |
|
Leonardo de Moura
|
4d32f8eb9d
|
feat: add arg conv tactic
|
2021-09-02 17:43:43 -07:00 |
|
Leonardo de Moura
|
d7537f252a
|
chore: remove unnecessay parser/elab
|
2021-09-02 17:29:32 -07:00 |
|
Leonardo de Moura
|
391366ef24
|
refactor: add annotation for displaying conv state
|
2021-09-02 15:52:11 -07:00 |
|
Leonardo de Moura
|
4df9983843
|
feat: lhs and rhs conv tactics
|
2021-09-02 15:05:51 -07:00 |
|