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
|
2aa882a416
|
chore: remove getElem', use custom delab
|
2022-09-21 06:21:00 -07:00 |
|
Mario Carneiro
|
553be10b90
|
fix: getElem' should be an abbrev
|
2022-09-21 06:21:00 -07:00 |
|
Mario Carneiro
|
3e83e28e8f
|
feat: injections with names
|
2022-09-20 17:36:35 -07:00 |
|
Mario Carneiro
|
a74892a36b
|
feat: multiple case
|
2022-09-20 14:15:37 -07:00 |
|
Mario Carneiro
|
65a861da68
|
feat: multiple case (part 1)
|
2022-09-20 14:15:37 -07:00 |
|
Mario Carneiro
|
8182f83929
|
doc: documentation for Init.Tactics
|
2022-08-17 14:44:40 -07:00 |
|
Leonardo de Moura
|
ef308e7f2c
|
chore: remove leftover notation
|
2022-08-15 06:25:35 -07:00 |
|
Leonardo de Moura
|
55bb8e905a
|
chore: binderIdent normalization
fixes #1411
|
2022-08-04 21:10:02 -07:00 |
|
Sebastian Ullrich
|
a44472962d
|
fix: replace uses of token antiquotations in tactics with with_annotate_state
|
2022-08-02 04:54:48 -07:00 |
|
Leonardo de Moura
|
99413a18ff
|
feat: add congr tactic
|
2022-08-01 18:44:07 -07:00 |
|
Leonardo de Moura
|
0156b59ef1
|
chore: enforce naming convention
|
2022-08-01 09:58:11 -07:00 |
|
Mario Carneiro
|
25aea1b723
|
doc: document all the tactics
|
2022-08-01 08:08:03 -07:00 |
|
Mario Carneiro
|
df85fee62c
|
chore: rename ac_refl to ac_rfl
|
2022-08-01 06:53:08 -07:00 |
|
Leonardo de Moura
|
97a5a88ae2
|
doc: add doc string to simp attribute parser
|
2022-07-27 06:34:55 -07:00 |
|
Sebastian Ullrich
|
5160cb7b0f
|
refactor: remove some unnecessary antiquotation kind annotations
|
2022-07-23 17:09:32 +02:00 |
|
Leonardo de Moura
|
4173a863d8
|
chore: cleanup
|
2022-07-10 09:43:12 -07:00 |
|
Leonardo de Moura
|
35018dbea2
|
feat: unexpanders for a[i], a[i]' h, a[i]!, and a[i]?
|
2022-07-10 06:47:23 -07:00 |
|
Leonardo de Moura
|
881589fc46
|
chore: remove parser workarounds
|
2022-07-09 16:42:39 -07:00 |
|
Leonardo de Moura
|
e4b358a01e
|
refactor: prepare to elaborate a[i] notation using typeclasses
|
2022-07-09 15:24:22 -07:00 |
|
Sebastian Ullrich
|
9816331562
|
chore: clean up bootstrapping cleanup
|
2022-06-28 16:28:36 +02:00 |
|
Sebastian Ullrich
|
77c6f433c7
|
chore: clean up bootstrapping workarounds
|
2022-06-28 16:01:07 +02:00 |
|
Sebastian Ullrich
|
89a101e9b8
|
refactor: remove group(·)s
|
2022-06-28 11:50:59 +02:00 |
|
Sebastian Ullrich
|
19c2644d88
|
chore: add more comments
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
d9cfda4893
|
refactor: make more use of quotations
Automatically fixes many TSyntax type errors
|
2022-06-27 22:37:02 +02:00 |
|
Sebastian Ullrich
|
fe22d84143
|
fix: unclear TSyntax breakage
|
2022-06-27 22:37:02 +02:00 |
|
Leonardo de Moura
|
986de33097
|
fix: fixes #1230
|
2022-06-20 09:58:27 -07:00 |
|
Leonardo de Moura
|
daeb271678
|
feat: update induction and cases syntax
We can now write
```
induction x with
| foo | bar => ...
| boo => ...
```
TODO: expand alternatives containing multiple LHSs.
|
2022-06-14 11:25:15 -07:00 |
|
Sebastian Ullrich
|
f9e2a65f75
|
chore: further cleanup
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
|
2022-06-07 16:37:45 -07:00 |
|
Sebastian Ullrich
|
fb2a2b3de2
|
fix: fixup previous commit
|
2022-06-07 16:37:45 -07:00 |
|
Sebastian Ullrich
|
ae7b895f7a
|
refactor: unname some unused variables
|
2022-06-07 16:37:45 -07:00 |
|
Leonardo de Moura
|
40fc64480a
|
feat: add tactic subst_vars
|
2022-05-28 16:19:34 -07:00 |
|
Sebastian Ullrich
|
c3a9831388
|
doc: document ‹t›
|
2022-05-18 10:32:06 +02:00 |
|
Leonardo de Moura
|
fc03b2fc31
|
feat: unfold ident,+
|
2022-05-09 07:09:53 -07:00 |
|
Leonardo de Moura
|
ecbc59c8d8
|
chore: split Notation.lean
|
2022-05-09 05:20:19 -07:00 |
|
Leonardo de Moura
|
df0e4808ec
|
feat: define tactic parsers using syntax command
|
2020-11-17 13:52:36 -08:00 |
|
Leonardo de Moura
|
8c4ac7ccc1
|
refactor: rename LeanInit ==> Meta, and reduce dependencies
|
2020-11-13 16:00:31 -08:00 |
|
Leonardo de Moura
|
65dafaf07c
|
fix: stdlib and tests
We also declare a few macros for the syntax command.
|
2020-11-12 07:12:30 -08:00 |
|
Leonardo de Moura
|
ef3f8c8723
|
feat: add funext tactic macro
|
2020-11-08 07:30:24 -08:00 |
|
Leonardo de Moura
|
7cbee83a8a
|
feat: add try tactic
|
2020-11-03 17:20:52 -08:00 |
|
Leonardo de Moura
|
b9a2885e65
|
feat: add repeat tactic
|
2020-11-03 17:20:52 -08:00 |
|
Leonardo de Moura
|
0032578d5b
|
feat: add have <ident> := <term> tactic macro
|
2020-10-29 20:39:40 -07:00 |
|
Leonardo de Moura
|
956a646a9c
|
chore: admit as a macro
|
2020-10-29 18:58:29 -07:00 |
|
Leonardo de Moura
|
0f3bd8abb4
|
feat: add rfl and decide! tactic macros
|
2020-10-29 16:42:22 -07:00 |
|