Aesop.Tree.Data

proven: the node is proven.
unprovable: the node is unprovable, i.e. it will never be proven regardless of any future expansions that might be performed.
unknown: neither of the above.

Every node starts in the unknown state and may later become either proven or unprovable. After this, the state does not change any more.

unknown: Aesop.NodeState
proven: Aesop.NodeState
unprovable: Aesop.NodeState

Instances For

source

instance Aesop.instInhabitedNodeState :

Inhabited Aesop.NodeState

Equations

Aesop.instInhabitedNodeState = { default := Aesop.NodeState.unknown }

source

instance Aesop.instBEqNodeState :

BEq Aesop.NodeState

Equations

Aesop.instBEqNodeState = { beq := Aesop.beqNodeState✝ }

source

instance Aesop.NodeState.instToStringNodeState :

ToString Aesop.NodeState

Equations

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

source

def Aesop.NodeState.isUnknown :

Aesop.NodeState → Bool

Equations

Aesop.NodeState.isUnknown x = match x with | Aesop.NodeState.unknown => true | x => false

source

def Aesop.NodeState.isProven :

Aesop.NodeState → Bool

Equations

Aesop.NodeState.isProven x = match x with | Aesop.NodeState.proven => true | x => false

source

def Aesop.NodeState.isUnprovable :

Aesop.NodeState → Bool

Equations

Aesop.NodeState.isUnprovable x = match x with | Aesop.NodeState.unprovable => true | x => false

source

def Aesop.NodeState.isIrrelevant :

Aesop.NodeState → Bool

Equations

Aesop.NodeState.isIrrelevant x = match x with | Aesop.NodeState.proven => true | Aesop.NodeState.unprovable => true | Aesop.NodeState.unknown => false

source

def Aesop.NodeState.toEmoji :

Aesop.NodeState → String

Equations

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

source

inductive Aesop.GoalState :

Type

A refinement of the NodeState, distinguishing between goals proven during normalisation and goals proven by a child rule application.

unknown: Aesop.GoalState
provenByRuleApplication: Aesop.GoalState
provenByNormalization: Aesop.GoalState
unprovable: Aesop.GoalState

Instances For

source

instance Aesop.instInhabitedGoalState :

Inhabited Aesop.GoalState

Equations

Aesop.instInhabitedGoalState = { default := Aesop.GoalState.unknown }

source

instance Aesop.instBEqGoalState :

BEq Aesop.GoalState

Equations

Aesop.instBEqGoalState = { beq := Aesop.beqGoalState✝ }

source

instance Aesop.GoalState.instToStringGoalState :

ToString Aesop.GoalState

Equations

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

source

def Aesop.GoalState.isProvenByRuleApplication :

Aesop.GoalState → Bool

Equations

Aesop.GoalState.isProvenByRuleApplication x = match x with | Aesop.GoalState.provenByRuleApplication => true | x => false

source

def Aesop.GoalState.isProvenByNormalization :

Aesop.GoalState → Bool

Equations

Aesop.GoalState.isProvenByNormalization x = match x with | Aesop.GoalState.provenByNormalization => true | x => false

source

def Aesop.GoalState.isProven :

Aesop.GoalState → Bool

Equations

Aesop.GoalState.isProven x = match x with | Aesop.GoalState.provenByRuleApplication => true | Aesop.GoalState.provenByNormalization => true | x => false

source

def Aesop.GoalState.isUnprovable :

Aesop.GoalState → Bool

Equations

Aesop.GoalState.isUnprovable x = match x with | Aesop.GoalState.unprovable => true | x => false

source

def Aesop.GoalState.isUnknown :

Aesop.GoalState → Bool

Equations

Aesop.GoalState.isUnknown x = match x with | Aesop.GoalState.unknown => true | x => false

source

def Aesop.GoalState.toNodeState :

Aesop.GoalState → Aesop.NodeState

Equations

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

source

def Aesop.GoalState.isIrrelevant (s : Aesop.GoalState) :

Bool

Equations

Aesop.GoalState.isIrrelevant s = Aesop.NodeState.isIrrelevant (Aesop.GoalState.toNodeState s)

source

def Aesop.GoalState.toEmoji :

Aesop.GoalState → String

Equations

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

source

inductive Aesop.NormalizationState :

Type

notNormal: Aesop.NormalizationState
normal: Lean.MVarId → Lean.Meta.SavedState → Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormalizationState
provenByNormalization: Lean.Meta.SavedState → Except Aesop.DisplayRuleName Aesop.UnstructuredScript → Aesop.NormalizationState

Instances For

Aesop.instInhabitedNormalizationState

source

instance Aesop.instInhabitedNormalizationState :

Inhabited Aesop.NormalizationState

Equations

Aesop.instInhabitedNormalizationState = { default := Aesop.NormalizationState.notNormal }

source

def Aesop.NormalizationState.isNormal :

Aesop.NormalizationState → Bool

Equations

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

source

def Aesop.NormalizationState.isProvenByNormalization :

Aesop.NormalizationState → Bool

Equations

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

source

def Aesop.NormalizationState.normalizedGoal? :

Aesop.NormalizationState → Option Lean.MVarId

Equations

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

source

inductive Aesop.GoalOrigin :

Type

A goal G can be added to the tree for three reasons:

G was produced by its parent rule as a subgoal. This is the most common reason.
G was copied because it contains some metavariables which were assigned by its parent rule. In this case, we record goal of which G is a copy. We also record the representative of the equivalence class of goals which are copies of each other. E.g. if goal 1 is copied to goal 2 and goal 2 is copied to goal 3, they are all part of the equivalence class with representative 1.