ink

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!

Equations

• Std.Tactic.unreachable = Lean.ParserDescr.node `Std.Tactic.unreachable 1024 (Lean.ParserDescr.nonReservedSymbol "unreachable!" false)

ink

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!

Equations

• Std.Tactic.unreachableConv = Lean.ParserDescr.node `Std.Tactic.unreachableConv 1024 (Lean.ParserDescr.nonReservedSymbol "unreachable!" false)