Documentation

Std.Lean.Tactic

Like evalTacticAt, but without restoring the goal list or pruning solved goals. Useful when these tasks are already being done in an outer loop.

Equations