def Std.Tactic.unreachable : Lean.ParserDescr

This tactic causes a panic when run (at compile time). (This is distinct from exact unreachable!, which inserts code which will panic at run time.)

It is intended for tests to assert that a tactic will never be executed, which is otherwise an unusual thing to do (and the unreachableTactic linter will give a warning if you do).

The unreachableTactic linter has a special exception for uses of unreachable!.

example : True := by trivial <;> unreachable!

def Std.Tactic.unreachableConv : Lean.ParserDescr

This tactic causes a panic when run (at compile time). (This is distinct from exact unreachable!, which inserts code which will panic at run time.)

It is intended for tests to assert that a tactic will never be executed, which is otherwise an unusual thing to do (and the unreachableTactic linter will give a warning if you do).

The unreachableTactic linter has a special exception for uses of unreachable!.

example : True := by trivial <;> unreachable!