Debugging support code for checking basic invariants.

def Lean.Meta.Grind.checkChild (e child : Expr) : GoalM Bool

Equations

• Lean.Meta.Grind.checkChild e child = do let __discr ← Lean.Meta.Grind.getRoot? child match __discr with | some childRoot => pure (Lean.Meta.Grind.isSameExpr childRoot e) | x => pure false

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

Checks basic invariants if grind.debug is enabled.

Equations

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

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

Equations

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