absurd タクティクを自作する

The tactic could be a little more helpful than the absurd term and try both argument orders:

macro "absurd " e₁:term:arg e₂:term:arg : tactic =>
  `(tactic|
    first
      | exact absurd $e₁ $e₂
      | exact absurd $e₂ $e₁
      | fail "could not find absurdity"
  )

example (p : Prop) (h : p) (h' : ¬ p) : 1 = 2 := by
  absurd h h'

example (p : Prop) (h : p) (h' : ¬ p) : 1 = 2 := by
  absurd h' h

example (p q : Prop) (h : p) (h' : ¬ q) : 1 = 2 := by
  absurd h' h
  -- error: could not find absurdity

Start from the proposed absurd tactic macro in the issue and run the three Lean examples to verify both argument orders and the failure case. Done means the tactic accepts either order for contradictory hypotheses and reports "could not find absurdity" when the hypotheses do not contradict.