From 4173a863d810a0401df342e09a830e54772c986e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Jul 2022 09:43:12 -0700 Subject: [PATCH] chore: cleanup --- src/Init/Data/Fin/Basic.lean | 2 +- src/Init/Tactics.lean | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index b65ac8548c..5c4827521d 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -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) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 7b822b3d67..a197f85805 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -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