Marking Nodes As Proven/Unprovable/Irrelevant

Irrelevant

def Aesop.Goal.isIrrelevantNoCache (g : Aesop.Goal) : BaseIO Bool

Equations

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

def Aesop.Rapp.isIrrelevantNoCache (r : Aesop.Rapp) : BaseIO Bool

Equations

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

def Aesop.MVarCluster.isIrrelevantNoCache (c : Aesop.MVarCluster) : BaseIO Bool

Equations

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

def Aesop.TreeRef.markSubtreeIrrelevant : Aesop.TreeRef → BaseIO Unit

Equations

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

def Aesop.GoalRef.markSubtreeIrrelevant (gref : Aesop.GoalRef) : BaseIO Unit

Equations

• Aesop.GoalRef.markSubtreeIrrelevant gref = Aesop.TreeRef.markSubtreeIrrelevant (Aesop.TreeRef.goal gref)

def Aesop.RappRef.markSubtreeIrrelevant (rref : Aesop.RappRef) : BaseIO Unit

Equations

• Aesop.RappRef.markSubtreeIrrelevant rref = Aesop.TreeRef.markSubtreeIrrelevant (Aesop.TreeRef.rapp rref)

def Aesop.MVarClusterRef.markSubtreeIrrelevant (cref : Aesop.MVarClusterRef) : BaseIO Unit

Equations

• Aesop.MVarClusterRef.markSubtreeIrrelevant cref = Aesop.TreeRef.markSubtreeIrrelevant (Aesop.TreeRef.mvarCluster cref)

Proven

def Aesop.Goal.isProvenByNormalizationNoCache (g : Aesop.Goal) : Bool

Equations

• Aesop.Goal.isProvenByNormalizationNoCache g = Aesop.NormalizationState.isProvenByNormalization (Aesop.Goal.normalizationState g)

def Aesop.Goal.isProvenByRuleApplicationNoCache (g : Aesop.Goal) : BaseIO Bool

Equations

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

def Aesop.Goal.isProvenNoCache (g : Aesop.Goal) : BaseIO Bool

Equations

• Aesop.Goal.isProvenNoCache g = (pure (Aesop.Goal.isProvenByNormalizationNoCache g) <||> Aesop.Goal.isProvenByRuleApplicationNoCache g)

def Aesop.Rapp.isProvenNoCache (r : Aesop.Rapp) : BaseIO Bool

Equations

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

def Aesop.MVarCluster.isProvenNoCache (c : Aesop.MVarCluster) : BaseIO Bool

Equations

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

def Aesop.GoalRef.markProvenByNormalization (gref : Aesop.GoalRef) : BaseIO Unit

Equations

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

def Aesop.RappRef.markProven (rref : Aesop.RappRef) : BaseIO Unit

Equations

• Aesop.RappRef.markProven rref = Aesop.markProvenCore (Aesop.TreeRef.rapp rref)

Unprovable

def Aesop.Goal.isUnprovableNoCache (g : Aesop.Goal) : BaseIO Bool

Equations

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

def Aesop.Rapp.isUnprovableNoCache (r : Aesop.Rapp) : BaseIO Bool

Equations

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

def Aesop.MVarCluster.isUnprovableNoCache (c : Aesop.MVarCluster) : BaseIO Bool

Equations

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

def Aesop.GoalRef.markUnprovable (gref : Aesop.GoalRef) : BaseIO Unit

Equations

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

def Aesop.GoalRef.markForcedUnprovable (gref : Aesop.GoalRef) : BaseIO Unit

Equations

• Aesop.GoalRef.markForcedUnprovable gref = do ST.Ref.modify gref fun (x : Aesop.Goal) => Aesop.Goal.setIsForcedUnprovable true x Aesop.GoalRef.markUnprovable gref

def Aesop.GoalRef.checkAndMarkUnprovable (gref : Aesop.GoalRef) : BaseIO Unit

Equations

• Aesop.GoalRef.checkAndMarkUnprovable gref = Aesop.markUnprovableCore (Aesop.TreeRef.goal gref)

Uncached Node States

def Aesop.Goal.stateNoCache (g : Aesop.Goal) : BaseIO Aesop.GoalState

Equations

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

def Aesop.Rapp.stateNoCache (r : Aesop.Rapp) : BaseIO Aesop.NodeState

Equations

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

def Aesop.MVarCluster.stateNoCache (c : Aesop.MVarCluster) : BaseIO Aesop.NodeState

Equations

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