Marking Nodes As Proven/Unprovable/Irrelevant

Irrelevant

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

Equations

• g.isIrrelevantNoCache = (pure g.state.isIrrelevant <||> do let __do_lift ← ST.Ref.get g.parent pure __do_lift.isIrrelevant)

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

Equations

• r.isIrrelevantNoCache = (pure r.state.isIrrelevant <||> do let __do_lift ← ST.Ref.get r.parent pure __do_lift.isIrrelevant)

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

Equations

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

def Aesop.TreeRef.markSubtreeIrrelevant : TreeRef → BaseIO Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Proven

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

Equations

• g.isProvenByNormalizationNoCache = g.normalizationState.isProvenByNormalization

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

Equations

• g.isProvenByRuleApplicationNoCache = Array.anyM (fun (rref : Aesop.RappRef) => do let __do_lift ← ST.Ref.get rref pure __do_lift.state.isProven) g.children

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

Equations

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

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

Equations

• r.isProvenNoCache = Array.allM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isProven) r.children

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

Equations

• c.isProvenNoCache = Array.anyM (fun (cref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isProven) c.goals

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

Equations

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

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

Equations

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

Unprovable

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

Equations

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

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

Equations

• r.isUnprovableNoCache = Array.anyM (fun (cref : Aesop.MVarClusterRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isUnprovable) r.children

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

Equations

• c.isUnprovableNoCache = Array.allM (fun (cref : Aesop.GoalRef) => do let __do_lift ← ST.Ref.get cref pure __do_lift.state.isUnprovable) c.goals

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

Equations

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

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

Equations

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

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

Equations

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

Uncached Node States

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

Equations

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

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

Equations

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

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

Equations

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