Sebastian Ullrich
|
dc60150b5a
|
chore: update domain
|
2023-09-20 15:13:27 -07:00 |
|
Mario Carneiro
|
776bff1948
|
fix: repeat conv should not auto-close the goal
|
2023-07-27 18:15:35 -04:00 |
|
Mario Carneiro
|
5661b15e35
|
fix: spacing and indentation fixes
|
2023-05-28 18:48:36 -07:00 |
|
Mario Carneiro
|
8b0699cd3b
|
fix: disable memoize in pattern conv
|
2022-12-19 06:21:54 -08:00 |
|
Sebastian Ullrich
|
a89b1b4b95
|
fix: use patternIgnore to ignore now-relevant tokens again
|
2022-10-28 21:25:47 +02:00 |
|
Mario Carneiro
|
d7d61bfb55
|
feat: use withoutPosition consistently (part 2)
|
2022-10-24 12:51:32 -07:00 |
|
Gabriel Ebner
|
0c2a5580cb
|
feat: enforce correct syntax kind in macros
|
2022-10-18 14:59:14 -07:00 |
|
Gabriel Ebner
|
fb4d90a58b
|
feat: dynamic quotations for categories
|
2022-10-18 14:59:14 -07:00 |
|
Sebastian Ullrich
|
d417c0238a
|
doc: normalize Init.Conv docs
|
2022-10-06 17:27:33 -07:00 |
|
Mario Carneiro
|
2a748d3035
|
fix: conv case => should close the goal conv-style
|
2022-09-28 14:24:44 -07:00 |
|
Mario Carneiro
|
b8ed329a5d
|
feat: add dsimp conv <- mathlib4
Co-authored-by: Moritz Doll <doll@uni-bremen.de>
|
2022-09-28 14:24:44 -07:00 |
|
Mario Carneiro
|
a09934c693
|
feat: more conv goal structuring tactics
|
2022-09-28 14:24:44 -07:00 |
|
Mario Carneiro
|
9b9998f5c8
|
feat: pattern (occs := ...) conv
|
2022-09-25 19:52:56 -07:00 |
|
Mario Carneiro
|
7dc0e1aa7d
|
fix: tweak formatter spacing for tactics
|
2022-09-25 06:40:56 -07:00 |
|
Mario Carneiro
|
3f229d5437
|
fix: add colGt
|
2022-09-21 18:04:31 -07:00 |
|
Mario Carneiro
|
ef0736c303
|
feat: multiple delta (part 2)
|
2022-09-21 18:04:31 -07:00 |
|
Mario Carneiro
|
90353d7fd7
|
feat: multiple delta, delta conv, unfold
|
2022-09-21 18:04:31 -07:00 |
|
Gabriel Ebner
|
2b5c1e397a
|
feat: use sepBy1Indent for conv blocks
|
2022-09-18 16:43:23 -07:00 |
|
Mario Carneiro
|
f5c5af1e86
|
doc: document all the syntax categories (#1401)
* chore: use Category declarations for builtin cats too
* doc: document all the syntax categories
* fix: fix test
|
2022-08-03 18:13:39 -07:00 |
|
Mario Carneiro
|
5f39370d94
|
chore: rename skip conv to rfl and add no-op skip
|
2022-08-01 13:54:36 -07:00 |
|
Mario Carneiro
|
f235cd8537
|
doc: document all the convs
|
2022-08-01 09:28:30 -07:00 |
|
Mario Carneiro
|
5ed3e580ef
|
fix: allow {} as conv
|
2022-08-01 08:47:51 -07:00 |
|
Mario Carneiro
|
25aea1b723
|
doc: document all the tactics
|
2022-08-01 08:08:03 -07:00 |
|
Sebastian Ullrich
|
5160cb7b0f
|
refactor: remove some unnecessary antiquotation kind annotations
|
2022-07-23 17:09:32 +02:00 |
|
Sebastian Ullrich
|
89a101e9b8
|
refactor: remove group(·)s
|
2022-06-28 11:50:59 +02:00 |
|
Sebastian Ullrich
|
a12cde41e1
|
chore: work around macro limitations
It would be nice if `macro` was as expressive as syntax quotations, but
right now it's not.
|
2022-06-27 22:37:02 +02:00 |
|
Leonardo de Moura
|
4d1c6dd557
|
feat: add zeta conv tactic
|
2022-06-22 19:15:10 -07:00 |
|
Jakob von Raumer
|
d7cb93e9e4
|
feat: allow conv mode's arg command to access implicit arguments
|
2022-06-14 16:15:38 -07:00 |
|
Sebastian Ullrich
|
8ffa07ab25
|
fix: goal state on conv =>
|
2022-06-07 17:43:16 +02:00 |
|
Sebastian Ullrich
|
74435013f4
|
chore: remove now-broken workarounds
|
2022-04-08 15:53:58 +02:00 |
|
Leonardo de Moura
|
799c701f56
|
fix: inconsistency between syntax and kind names
TODO: remove staging workarounds
see #1090
|
2022-04-01 11:20:16 -07:00 |
|
Leonardo de Moura
|
b1b4705c14
|
feat: add unfold tactic parsers
|
2022-01-07 13:51:45 -08:00 |
|
Leonardo de Moura
|
fbdb68b669
|
feat: conv in conv
Featured suggested at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pattern.20matching.20lambda.20body.20in.20conv/near/257193307
|
2021-10-22 13:53:56 -07:00 |
|
Leonardo de Moura
|
7f660af4c6
|
feat: add repeat tactic to conv mode
|
2021-10-06 14:05:44 -07:00 |
|
Leonardo de Moura
|
0a898965a3
|
chore: use snake_case for user-facing tactic names
|
2021-09-16 10:23:12 -07:00 |
|
Leonardo de Moura
|
c2a5e37c60
|
feat: simp discharger
|
2021-09-16 10:11:27 -07:00 |
|
Leonardo de Moura
|
d2240a99e5
|
feat: add erw tactic back as a macro
|
2021-09-12 19:29:12 -07:00 |
|
Leonardo de Moura
|
42436254ee
|
fix: code
|
2021-09-12 19:11:21 -07:00 |
|
Leonardo de Moura
|
bfa1c86b24
|
feat: add optional config parser to rewrite tactics
|
2021-09-12 19:05:15 -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
|
b5b5370181
|
feat: add delta to conv mode
|
2021-09-09 13:07:33 -07:00 |
|
Leonardo de Moura
|
53a3831fd5
|
feat: add apply conv macro
|
2021-09-03 20:23:15 -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
|
44e7033c27
|
feat: add support for forall_congr at conv
|
2021-09-03 16:57:15 -07:00 |
|
Leonardo de Moura
|
18bcc458d0
|
feat: add 'enter' conv tactic macro
|
2021-09-03 08:11:37 -07:00 |
|
Leonardo de Moura
|
b5b5ef6fdf
|
feat: add funext conv tactic
|
2021-09-03 08:00:37 -07:00 |
|
Leonardo de Moura
|
397774157f
|
feat: nested tactic support in conv mode
|
2021-09-02 19:12:05 -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 |
|