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.

Equations

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

Instances For

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

Checks invariants if `grind.debug` is enabled.

Equations

- goal.checkInvariants expensive = discard (Lean.Meta.Grind.GoalM.run' goal (Lean.Meta.Grind.checkInvariants expensive))

Instances For