Documentation

Lean.Meta.Tactic.Grind.Util

Throws an exception if target of the given goal contains metavariables.

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

Throws an exception if target is not a proposition.

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

Unfold all reducible declarations occurring in e.

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

Unfold all reducible declarations occurring in the goal's target.

Equations

Abstract nested proofs occurring in the goal's target.

Beta-reduce the goal's target.

Equations

If the target is not False, apply byContradiction.

Clear auxiliary decls used to encode recursive declarations. grind eliminates them to ensure they are not accidentally used by its proof automation.