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

chore: simplify tactic macro

Browse source 
The `[inlineIfReduce]` at `List.toArrayAux` is currently very
expensive, and this example produces a deep recursion when inlining
the `List.toArrayAux` applications.
This commit is contained in:
Leonardo de Moura 2022-09-24 19:53:04 -07:00
parent ce12ecfe13
commit f9abcae4e4
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/wfEqnsIssue.lean
View file

@ -62,8 +62,7 @@ theorem Nat.le_add_right_of_le (n m : Nat) : n ≤ m → n ≤ m + k :=
macro_rules
| `(tactic| decreasing_tactic) =>
`(tactic|
(simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
(simp_wf
repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
simp [Nat.add_comm (n := 1), Nat.succ_add, Nat.mul_succ]
try apply Nat.lt_succ_of_le