Documentation

Lean.Meta.Tactic.Grind.Inv

Debugging support code for checking basic invariants.

Checks invariants if grind.debug is enabled.

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

    Checks invariants if grind.debug is enabled.

    Equations
    Instances For