syntax "foo" : tactic

macro_rules | `(tactic| foo) => `(tactic| assumption)
macro_rules | `(tactic| foo) => `(tactic| apply Nat.pred_lt; assumption)
macro_rules | `(tactic| foo) => `(tactic| contradiction)

example (i : Nat) (h : i - 1 < i) : i - 1 < i := by
  foo

example (i : Nat) (h : i ≠ 0) : i - 1 < i := by
  foo

example (i : Nat) (h : False) : i - 1 < i := by
  foo