Documentation

Lean.Meta.Tactic.Grind.Inv

Debugging support code for checking basic invariants.

source
def Lean.Meta.Grind.checkInvariants (expensive : Bool := false) :
GoalM Unit

Checks invariants if grind.debug is enabled.

Instances For
    source
    def Lean.Meta.Grind.Goal.checkInvariants (goal : Goal) (expensive : Bool := false) :
    GrindM Unit

    Checks invariants if grind.debug is enabled.

    Instances For