Ensuring failure of a top-level command

Stream: Is there code for X?

[Youngju Song]

For some sanity check and documentation purpose, I would like to have some commands that ensures some top-level command fails, like #fail in the following:

#check (-1: Nat) -- fails and aborts compilation
#check (-1: Int) -- does not fail
#fail (#check (-1: Nat)) -- does not fail
#fail (#check (-1: Int)) -- fails and aborts compilation

would there be a command for this in Lean4?

[Damiano Testa]

There is a tactic success_if_fail_with_msg

import Mathlib

/--
info: Found 1 use among 2002 syntax declarations
---

Mathlib.Tactic.successIfFailWithMsg:
  'success_if_fail_with_msg'
---
-/
#guard_msgs in
#find_syntax "success_if"

but I do not think that there is exactly the command that you want. You can always do

/--
error: failed to synthesize
  Neg ℕ
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
#check (-1: Nat)

#guard_msgs(drop error) in
#check (-1: Nat)

though.

[Youngju Song]

@Damiano Testa Thank you for the information!

[Youngju Song]

For top-level commands, maybe I should look into the definition of guard_msgs and do some hack.
For tactics, it seems the success_if tactic you mentioned and its variant fail_if_success will do the job. Thanks!

[Youngju Song]

I found check_failure command that corresponds to #fail (#check _) in my original question. I should start playing with this