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

Equations

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

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

Equations

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

def Aesop.MVarClusterRef.checkAcyclic.go {α : Type} (visited : IO.Ref (Array (IO.Ref α))) (current : IO.Ref α) : Lean.CoreM Bool

Equations

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

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

Equations

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

def Aesop.MVarClusterRef.checkConsistentParentChildLinks.err : ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception)) PUnit

Equations

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

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

Equations

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

@[inline]

def Aesop.MVarClusterRef.checkState.go {σ : Type} [BEq σ] [ToString σ] (id : String) (expected actual : σ) : Lean.CoreM Unit

Equations

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

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

Equations

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

@[inline]

def Aesop.MVarClusterRef.checkIrrelevance.go (id : String) (expected actual : Bool) : Lean.CoreM Bool

Equations

• One or more equations did not get rendered due to their size.
• Aesop.MVarClusterRef.checkIrrelevance.go id expected actual = pure true

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

Equations

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

def Aesop.MVarClusterRef.checkMVars.getParentInfo (r : Aesop.Rapp) : Lean.CoreM (Lean.MVarId × Lean.Meta.SavedState)

Equations

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

def Aesop.MVarClusterRef.checkMVars.checkAssignedMVars (r : Aesop.Rapp) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkMVars.checkDroppedMVars (r : Aesop.Rapp) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkMVars.checkGoalMVars (rootMetaState : Lean.Meta.SavedState) (g : Aesop.Goal) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkMVars.checkNormMVars (rootMetaState : Lean.Meta.SavedState) (g : Aesop.Goal) : Lean.MetaM Unit

Equations

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

def Aesop.MVarClusterRef.checkIntroducedMVars (root : Aesop.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 : Aesop.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 : Aesop.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 PUnit.unit

def Aesop.checkInvariantsIfEnabled : Aesop.TreeM Unit

Equations

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