int-y1
ce4ae37c19
chore: fix more typos in comments
2023-10-08 14:37:34 -07:00
Scott Morrison
c318d5817d
feat: allow configuring occs in rw
2023-09-13 12:03:18 -07:00
Floris van Doorn
1a6663a41b
chore: write "|-" as "|" noWs "-" ( #2299 )
...
* remove |- as an alias for ⊢
* revert false positive |->
* fix docstring
* undo previous changes
* [unchecked] use suggestion
* next attempt
* add test
2023-07-14 09:48:20 -07:00
Mario Carneiro
43f6d0a761
feat: implement have this (part 1)
2023-06-02 16:19:02 +02:00
Mario Carneiro
5661b15e35
fix: spacing and indentation fixes
2023-05-28 18:48:36 -07:00
Scott Morrison
ac7c447855
chore: update src/Init/Tactics.lean
2023-04-19 07:15:08 -07:00
Scott Morrison
96969363e6
chore: modify misleading doc-string for repeat tactic
2023-04-18 15:56:49 +02:00
Jeremy Salwen
60f30addc7
doc: add more detail to the split tactic docs ( #1988 )
...
Co-authored-by: Mac <tydeu@hatpress.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2023-01-09 13:12:39 +01:00
Mario Carneiro
9b572d4e20
chore: make <;> left associative
2022-11-23 07:44: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
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -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
Mario Carneiro
a09934c693
feat: more conv goal structuring tactics
2022-09-28 14:24:44 -07:00
Mario Carneiro
fa13d7321f
feat: generalize e = x at h
2022-09-25 06:42:20 -07:00
Mario Carneiro
7dc0e1aa7d
fix: tweak formatter spacing for tactics
2022-09-25 06:40:56 -07:00
Mario Carneiro
b8cf796941
feat: if _ : cond then t else e syntax
2022-09-22 11:01:08 -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
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
