Marking Nodes As Proven/Unprovable/Irrelevant

Irrelevant

def Aesop.Goal.isIrrelevantNoCache (g : Aesop.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 : Aesop.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 : 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

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

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

Equations

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

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

Equations

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

Proven

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

Equations

• g.isProvenByNormalizationNoCache = g.normalizationState.isProvenByNormalization

def Aesop.Goal.isProvenByRuleApplicationNoCache (g : Aesop.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 0

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

Equations

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

def Aesop.Rapp.isProvenNoCache (r : Aesop.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 0

def Aesop.MVarCluster.isProvenNoCache (c : Aesop.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 0

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

• rref.markProven = 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

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

def Aesop.MVarCluster.isUnprovableNoCache (c : Aesop.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 0

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

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

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

Equations

• gref.checkAndMarkUnprovable = 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.