max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-10 09:43:12 -07:00
parent c82f74d094
commit 4173a863d8
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Fin/Basic.lean
View file

@ -121,4 +121,4 @@ instance [GetElem Cont Nat Elem Dom] : GetElem Cont (Fin n) Elem fun xs i => Dom
getElem xs i h := getElem xs i.1 h
macro_rules
| `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; (first | assumption | simp (config := { arith := true })); done)
| `(tactic| get_elem_tactic_trivial) => `(tactic| apply Fin.val_lt_of_le; get_elem_tactic_trivial; done)

3
src/Init/Tactics.lean
View file

@ -431,8 +431,7 @@ macro "‹" type:term "›" : term => `((by assumption : $type))
syntax "get_elem_tactic_trivial" : tactic -- extensible tactic
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| trivial)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| decide)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| assumption)
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
macro "get_elem_tactic" : tactic =>
`(first