From d2888a49d7a32a8dc8bcd3a658ffe7127ba4fde2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jun 2022 16:36:54 -0700 Subject: [PATCH] chore: remove old hack that is not needed anymore --- src/Init/WFTactics.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 677a21f701..e26d725e95 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -16,8 +16,6 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption) macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assumption) -- i-1 < i if i ≠ 0 -macro_rules | `(tactic| decreasing_trivial) => `(tactic| decide) -- e.g., 0 < 1 -macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.lt_succ_self) -- i < i+1 macro "decreasing_with " ts:tacticSeq : tactic => `((simp_wf