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

chore: remove old hack that is not needed anymore

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-15 16:36:54 -07:00
parent 3228db29dd
commit d2888a49d7
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/WFTactics.lean
View file

@ -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