fail

fail always fails.

This is sometimes useful if you’re building a complex tactic with try-catch behavior.

(* Simple usage *)
fail.

Before

=========================
1/1
True

fail.

After

Error: Tactic failure.