Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.
For example, in
example : True := by trivial <;> done, the tactic
done is never executed
trivial produces no subgoals; you could put
or anything else there and no error would result.
A common source of such things is
simp <;> tac in the case that
simp improves and
closes a subgoal that was previously being closed by
Gets the value of the
Is this a syntax kind that contains intentionally unevaluated tactic subterms?
Adds a new syntax kind whose children will be ignored by the
This should be called from an
The main entry point to the unreachable tactic linter.
- One or more equations did not get rendered due to their size.