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!
Instances For
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!