def Aesop.MVarClusterRef.checkIds (root : MVarClusterRef) : Lean.CoreM Unit

Equations

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

def Aesop.MVarClusterRef.checkAcyclic (root : MVarClusterRef) : Lean.CoreM Unit

Equations

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

def Aesop.MVarClusterRef.checkConsistentParentChildLinks (root : MVarClusterRef) : Lean.CoreM Unit

Equations

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

def Aesop.MVarClusterRef.checkState (root : MVarClusterRef) : Lean.CoreM Unit

Equations

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

def Aesop.MVarClusterRef.checkIrrelevance (root : MVarClusterRef) : Lean.CoreM Unit

Equations

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

def Aesop.MVarClusterRef.checkMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkIntroducedMVars (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkInvariants (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkInvariantsIfEnabled (root : MVarClusterRef) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM Unit

Equations

• root.checkInvariantsIfEnabled rootMetaState = do let __do_lift ← Aesop.Check.tree.isEnabled if __do_lift = true then root.checkInvariants rootMetaState else pure ()

def Aesop.checkInvariantsIfEnabled : TreeM Unit

Equations

• Aesop.checkInvariantsIfEnabled = do let __do_lift ← Aesop.getRootMVarCluster let __do_lift_1 ← Aesop.getRootMetaState liftM (__do_lift.checkInvariantsIfEnabled __do_lift_1)