How to represent definition fails?

Stream: new members

[Hyunwoo Lee]

In Coq you can deliberately show a rejected definition without breaking the build, e.g.:

Fail Definition foo := 1 + true.

This makes the compiler succeed while still demonstrating that the definition is ill-typed.

Is there an equivalent in Lean (Lean 4/Mathlib)? I’d like to include an example that must fail type-checking without causing the whole file to fail.

[Robin Arnez]

#guard_msgs (drop error) in?

[Robin Arnez]

Or even better, just #guard_msgs in and then use the code action to put the error message above the definition

[Robin Arnez]

e.g.

/--
error: failed to synthesize
  HAdd Nat Bool ?m.1

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
example := 1 + true

[Hyunwoo Lee]

Then does it only success when given error message is same as actual error mesaage?