Debugging support code for checking basic invariants.
Checks invariants if grind.debug
is enabled.
Equations
- goal.checkInvariants expensive = discard (Lean.Meta.Grind.GoalM.run' goal (Lean.Meta.Grind.checkInvariants expensive))
Debugging support code for checking basic invariants.
Checks invariants if grind.debug
is enabled.