Documentation

Batteries.Linter.UnreachableTactic

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 because trivial produces no subgoals; you could put sorry or apply I_don't_exist 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 tac.

@[reducible, inline]

The monad for collecting used tactic syntaxes.

Equations
Instances For

    A list of blacklisted syntax kinds, which are expected to have subterms that contain unevaluated tactics.

    Is this a syntax kind that contains intentionally unevaluated tactic subterms?

    Equations
    Instances For

      Adds a new syntax kind whose children will be ignored by the unreachableTactic linter. This should be called from an initialize block.

      Equations
      Instances For
        @[specialize #[]]

        Accumulates the set of tactic syntaxes that should be evaluated at least once.

        Search for tactic executions in the info tree and remove executed tactic syntaxes.

        Search for tactic executions in the info tree and remove executed tactic syntaxes.

        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 because trivial produces no subgoals; you could put sorry or apply I_don't_exist 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 tac.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For