Zulip Chat Archive

Stream: mathlib4

Topic: tests that expect failure


Arthur Paulino (Feb 06 2022 at 19:22):

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

Yakov Pechersky (Feb 06 2022 at 19:23):

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 (Feb 06 2022 at 19:25):

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


Last updated: Dec 20 2023 at 11:08 UTC