tests that expect failure

Stream: mathlib4

[Arthur Paulino]

Is it possible to write tests that succeed iff an specific error happens?

[Yakov Pechersky]

fail_if_success:
https://github.com/leanprover-community/mathlib4/pull/182/files#diff-27e449921b8f54090ed861ed84a990bc7a4e41e9a95c99e50dbea1256205541fR20-R27

example (x : (α × β) × γ) : True := by
  fail_if_success rcases x with ⟨a, b, c⟩
  fail_if_success rcases x with ⟨⟨a:β, b⟩, c⟩
  rcases x with ⟨⟨a:α, b⟩, c⟩
  guard_hyp a : α
  guard_hyp b : β
  guard_hyp c : γ
  trivial

[Arthur Paulino]

Nice! Maybe it can be improved to receive an optional error message so that it must fail in a specific way