Node IDs

structure Aesop.GoalId : Type

• toNat : Nat

instance Aesop.instInhabitedGoalId : Inhabited Aesop.GoalId

Equations

• Aesop.instInhabitedGoalId = { default := { toNat := default } }

instance Aesop.instDecidableEqGoalId : DecidableEq Aesop.GoalId

Equations

• Aesop.instDecidableEqGoalId = Aesop.decEqGoalId✝

def Aesop.GoalId.zero : Aesop.GoalId

Equations

• Aesop.GoalId.zero = { toNat := 0 }

def Aesop.GoalId.one : Aesop.GoalId

Equations

• Aesop.GoalId.one = { toNat := 1 }

def Aesop.GoalId.succ : Aesop.GoalId → Aesop.GoalId

Equations

• Aesop.GoalId.succ x = match x with | { toNat := n } => { toNat := n + 1 }

def Aesop.GoalId.dummy : Aesop.GoalId

Equations

• Aesop.GoalId.dummy = { toNat := 1000000000000000 }

instance Aesop.GoalId.instLTGoalId : LT Aesop.GoalId

Equations

• Aesop.GoalId.instLTGoalId = { lt := fun n m => n.toNat < m.toNat }

instance Aesop.GoalId.instDecidableRelGoalIdLtInstLTGoalId : DecidableRel fun x x_1 => x < x_1

Equations

• Aesop.GoalId.instDecidableRelGoalIdLtInstLTGoalId n m = inferInstanceAs (Decidable (n.toNat < m.toNat))

instance Aesop.GoalId.instToStringGoalId : ToString Aesop.GoalId

Equations

• Aesop.GoalId.instToStringGoalId = { toString := fun n => toString n.toNat }

instance Aesop.GoalId.instHashableGoalId : Hashable Aesop.GoalId

Equations

• Aesop.GoalId.instHashableGoalId = { hash := fun n => hash n.toNat }

Rule Application IDs

structure Aesop.RappId : Type

• toNat : Nat

instance Aesop.instInhabitedRappId : Inhabited Aesop.RappId

Equations

• Aesop.instInhabitedRappId = { default := { toNat := default } }

instance Aesop.instDecidableEqRappId : DecidableEq Aesop.RappId

Equations

• Aesop.instDecidableEqRappId = Aesop.decEqRappId✝

def Aesop.RappId.zero : Aesop.RappId

Equations

• Aesop.RappId.zero = { toNat := 0 }

def Aesop.RappId.succ : Aesop.RappId → Aesop.RappId

Equations

• Aesop.RappId.succ x = match x with | { toNat := n } => { toNat := n + 1 }

def Aesop.RappId.one : Aesop.RappId

Equations

• Aesop.RappId.one = { toNat := 1 }

def Aesop.RappId.dummy : Aesop.RappId

Equations

• Aesop.RappId.dummy = { toNat := 1000000000000000 }

instance Aesop.RappId.instLTRappId : LT Aesop.RappId

Equations

• Aesop.RappId.instLTRappId = { lt := fun n m => n.toNat < m.toNat }

instance Aesop.RappId.instDecidableRelRappIdLtInstLTRappId : DecidableRel fun x x_1 => x < x_1

Equations

• Aesop.RappId.instDecidableRelRappIdLtInstLTRappId n m = inferInstanceAs (Decidable (n.toNat < m.toNat))

instance Aesop.RappId.instToStringRappId : ToString Aesop.RappId

Equations

• Aesop.RappId.instToStringRappId = { toString := fun n => toString n.toNat }

instance Aesop.RappId.instHashableRappId : Hashable Aesop.RappId

Equations

• Aesop.RappId.instHashableRappId = { hash := fun n => hash n.toNat }

Iterations

def Aesop.Iteration : Type

Equations

• Aesop.Iteration = Nat

@[inline]

def Aesop.Iteration.one : Aesop.Iteration

Equations

• Aesop.Iteration.one = Aesop.Iteration.ofNat 1

@[inline]

def Aesop.Iteration.succ (i : Aesop.Iteration) : Aesop.Iteration

Equations

• Aesop.Iteration.succ i = Aesop.Iteration.ofNat (Aesop.Iteration.toNat i + 1)

def Aesop.Iteration.none : Aesop.Iteration

Equations

• Aesop.Iteration.none = Aesop.Iteration.ofNat 0

instance Aesop.Iteration.instDecidableEqIteration : DecidableEq Aesop.Iteration

Equations

• Aesop.Iteration.instDecidableEqIteration = inferInstanceAs (DecidableEq Nat)

instance Aesop.Iteration.instToStringIteration : ToString Aesop.Iteration

Equations

• Aesop.Iteration.instToStringIteration = inferInstanceAs (ToString Nat)

instance Aesop.Iteration.instLTIteration : LT Aesop.Iteration

Equations

• Aesop.Iteration.instLTIteration = inferInstanceAs (LT Nat)

instance Aesop.Iteration.instLEIteration : LE Aesop.Iteration

Equations

• Aesop.Iteration.instLEIteration = inferInstanceAs (LE Nat)

instance Aesop.Iteration.instDecidableRelIterationLtInstLTIteration : DecidableRel fun x x_1 => x < x_1

Equations

• Aesop.Iteration.instDecidableRelIterationLtInstLTIteration = inferInstanceAs (DecidableRel fun x x_1 => x < x_1)

instance Aesop.Iteration.instDecidableRelIterationLeInstLEIteration : DecidableRel fun x x_1 => x ≤ x_1

Equations

• Aesop.Iteration.instDecidableRelIterationLeInstLEIteration = inferInstanceAs (DecidableRel fun x x_1 => x ≤ x_1)

The Tree

inductive Aesop.NodeState : Type

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

At each point during the search, every node of the tree (goal, rapp or mvar cluster) is in one of these states:

• 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.

instance Aesop.instInhabitedNodeState : Inhabited Aesop.NodeState

Equations

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

instance Aesop.instBEqNodeState : BEq Aesop.NodeState

Equations

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

instance Aesop.NodeState.instToStringNodeState : ToString Aesop.NodeState

Equations

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

def Aesop.NodeState.isUnknown : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.isProven : Aesop.NodeState → Bool

Equations

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

def Aesop.NodeState.isUnprovable : Aesop.NodeState → Bool

Equations

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

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

def Aesop.NodeState.toEmoji : Aesop.NodeState → String

Equations

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

inductive Aesop.GoalState : Type

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

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

instance Aesop.instInhabitedGoalState : Inhabited Aesop.GoalState

Equations

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

instance Aesop.instBEqGoalState : BEq Aesop.GoalState

Equations

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

instance Aesop.GoalState.instToStringGoalState : ToString Aesop.GoalState

Equations

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

def Aesop.GoalState.isProvenByRuleApplication : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isProvenByNormalization : Aesop.GoalState → Bool

Equations

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

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

def Aesop.GoalState.isUnprovable : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.isUnknown : Aesop.GoalState → Bool

Equations

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

def Aesop.GoalState.toNodeState : Aesop.GoalState → Aesop.NodeState

Equations

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

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

Equations

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

def Aesop.GoalState.toEmoji : Aesop.GoalState → String

Equations

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

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

instance Aesop.instInhabitedNormalizationState : Inhabited Aesop.NormalizationState

Equations

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

def Aesop.NormalizationState.isNormal : Aesop.NormalizationState → Bool

Equations

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

def Aesop.NormalizationState.isProvenByNormalization : Aesop.NormalizationState → Bool

Equations

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

inductive Aesop.GoalOrigin : Type

• subgoal: Aesop.GoalOrigin
• copied: Aesop.GoalId → Aesop.GoalId → Aesop.GoalOrigin
• droppedMVar: Aesop.GoalOrigin

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

1. G was produced by its parent rule as a subgoal. This is the most common reason.
2. 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.

instance Aesop.instInhabitedGoalOrigin : Inhabited Aesop.GoalOrigin

Equations

• Aesop.instInhabitedGoalOrigin = { default := Aesop.GoalOrigin.subgoal }

def Aesop.GoalOrigin.originalGoalId? : Aesop.GoalOrigin → Option Aesop.GoalId

Equations

• Aesop.GoalOrigin.originalGoalId? x = match x with | Aesop.GoalOrigin.copied from rep => some rep | x => none

def Aesop.GoalOrigin.toString : Aesop.GoalOrigin → String

Equations

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

structure Aesop.GoalData (Rapp : Type) (MVarCluster : Type) : Type

• id : Aesop.GoalId
• parent : IO.Ref MVarCluster
• children : Array (IO.Ref Rapp)
• origin : Aesop.GoalOrigin
• depth : Nat
• state : Aesop.GoalState
• isIrrelevant : Bool
• isForcedUnprovable : Bool
• preNormGoal : Lean.MVarId
• normalizationState : Aesop.NormalizationState
• mvars : Aesop.UnorderedArraySet Lean.MVarId
• successProbability : Aesop.Percent
• addedInIteration : Aesop.Iteration
• lastExpandedInIteration : Aesop.Iteration
• unsafeRulesSelected : Bool
• unsafeQueue : Aesop.UnsafeQueue
• failedRapps : Array Aesop.RegularRule

instance Aesop.instNonemptyGoalData : ∀ {Rapp MVarCluster : Type} [inst : Nonempty MVarCluster], Nonempty (Aesop.GoalData Rapp MVarCluster)

Equations

• @Aesop.instNonemptyGoalData = @Aesop.instNonemptyGoalData.proof_1

structure Aesop.MVarClusterData (Goal : Type) (Rapp : Type) : Type

• parent? : Option (IO.Ref Rapp)
• goals : Array (IO.Ref Goal)
• isIrrelevant : Bool
• state : Aesop.NodeState

instance Aesop.instInhabitedMVarClusterData : {a a_1 : Type} → Inhabited (Aesop.MVarClusterData a a_1)

Equations

• Aesop.instInhabitedMVarClusterData = { default := { parent? := default, goals := default, isIrrelevant := default, state := default } }

structure Aesop.RappData (Goal : Type) (MVarCluster : Type) : Type

• id : Aesop.RappId
• parent : IO.Ref Goal
• children : Array (IO.Ref MVarCluster)
• state : Aesop.NodeState
• isIrrelevant : Bool
• appliedRule : Aesop.RegularRule
• scriptBuilder? : Option Aesop.RuleTacScriptBuilder
• originalSubgoals : Array Lean.MVarId
• successProbability : Aesop.Percent
• metaState : Lean.Meta.SavedState
• introducedMVars : Aesop.UnorderedArraySet Lean.MVarId
• assignedMVars : Aesop.UnorderedArraySet Lean.MVarId

instance Aesop.instNonemptyRappData : ∀ {Goal : Type} [inst : Nonempty Goal] {MVarCluster : Type}, Nonempty (Aesop.RappData Goal MVarCluster)

Equations

• @Aesop.instNonemptyRappData = @Aesop.instNonemptyRappData.proof_1

unsafe inductive Aesop.GoalUnsafe : Type

• mk: Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Aesop.GoalUnsafe

unsafe inductive Aesop.MVarClusterUnsafe : Type

• mk: Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Aesop.MVarClusterUnsafe

unsafe inductive Aesop.RappUnsafe : Type

• mk: Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Aesop.RappUnsafe

structure Aesop.TreeSpec : Type 1

• Goal : Type
• Rapp : Type
• MVarCluster : Type
• introGoal : Aesop.GoalData s.Rapp s.MVarCluster → s.Goal
• elimGoal : s.Goal → Aesop.GoalData s.Rapp s.MVarCluster
• introRapp : Aesop.RappData s.Goal s.MVarCluster → s.Rapp
• elimRapp : s.Rapp → Aesop.RappData s.Goal s.MVarCluster
• introMVarCluster : Aesop.MVarClusterData s.Goal s.Rapp → s.MVarCluster
• elimMVarCluster : s.MVarCluster → Aesop.MVarClusterData s.Goal s.Rapp

instance Aesop.instNonemptyTreeSpec : Nonempty Aesop.TreeSpec

Equations

• Aesop.instNonemptyTreeSpec = Aesop.instNonemptyTreeSpec.proof_1

unsafe def Aesop.treeImpl : Aesop.TreeSpec

Equations

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

@[implemented_by Aesop.treeImpl]

opaque Aesop.tree : Aesop.TreeSpec

def Aesop.Goal : Type

Equations

• Aesop.Goal = Aesop.tree.Goal

def Aesop.Rapp : Type

Equations

• Aesop.Rapp = Aesop.tree.Rapp

def Aesop.MVarCluster : Type

Equations

• Aesop.MVarCluster = Aesop.tree.MVarCluster

@[inline, reducible]

abbrev Aesop.GoalRef : Type

Equations

• Aesop.GoalRef = IO.Ref Aesop.Goal

@[inline, reducible]

abbrev Aesop.RappRef : Type

Equations

• Aesop.RappRef = IO.Ref Aesop.Rapp

@[inline, reducible]

abbrev Aesop.MVarClusterRef : Type

Equations

• Aesop.MVarClusterRef = IO.Ref Aesop.MVarCluster

@[inline]

def Aesop.MVarCluster.mk : Aesop.MVarClusterData Aesop.Goal Aesop.Rapp → Aesop.MVarCluster

Equations

• Aesop.MVarCluster.mk = Aesop.tree.introMVarCluster

instance Aesop.MVarCluster.instNonemptyMVarCluster : Nonempty Aesop.MVarCluster

Equations

• Aesop.MVarCluster.instNonemptyMVarCluster = Aesop.MVarCluster.instNonemptyMVarCluster.proof_1

@[inline]

def Aesop.MVarCluster.elim : Aesop.MVarCluster → Aesop.MVarClusterData Aesop.Goal Aesop.Rapp

Equations

• Aesop.MVarCluster.elim = Aesop.tree.elimMVarCluster

@[inline]

def Aesop.MVarCluster.modify (f : Aesop.MVarClusterData Aesop.Goal Aesop.Rapp → Aesop.MVarClusterData Aesop.Goal Aesop.Rapp) (c : Aesop.MVarCluster) : Aesop.MVarCluster

Equations

• Aesop.MVarCluster.modify f c = Aesop.MVarCluster.mk (f (Aesop.MVarCluster.elim c))

@[inline]

def Aesop.MVarCluster.parent? (c : Aesop.MVarCluster) : Option Aesop.RappRef

Equations

• Aesop.MVarCluster.parent? c = (Aesop.MVarCluster.elim c).parent?

@[inline]

def Aesop.MVarCluster.setParent (parent? : Option Aesop.RappRef) (c : Aesop.MVarCluster) : Aesop.MVarCluster

Equations

• Aesop.MVarCluster.setParent parent? c = Aesop.MVarCluster.modify (fun c => { parent? := parent?, goals := c.goals, isIrrelevant := c.isIrrelevant, state := c.state }) c

@[inline]

def Aesop.MVarCluster.goals (c : Aesop.MVarCluster) : Array Aesop.GoalRef

Equations

• Aesop.MVarCluster.goals c = (Aesop.MVarCluster.elim c).goals

@[inline]

def Aesop.MVarCluster.setGoals (goals : Array Aesop.GoalRef) (c : Aesop.MVarCluster) : Aesop.MVarCluster

Equations

• Aesop.MVarCluster.setGoals goals c = Aesop.MVarCluster.modify (fun c => { parent? := c.parent?, goals := goals, isIrrelevant := c.isIrrelevant, state := c.state }) c

@[inline]

def Aesop.MVarCluster.isIrrelevant (c : Aesop.MVarCluster) : Bool

Equations

• Aesop.MVarCluster.isIrrelevant c = (Aesop.MVarCluster.elim c).isIrrelevant

@[inline]

def Aesop.MVarCluster.setIsIrrelevant (isIrrelevant : Bool) (c : Aesop.MVarCluster) : Aesop.MVarCluster

Equations

• Aesop.MVarCluster.setIsIrrelevant isIrrelevant c = Aesop.MVarCluster.modify (fun c => { parent? := c.parent?, goals := c.goals, isIrrelevant := isIrrelevant, state := c.state }) c

@[inline]

def Aesop.MVarCluster.state (c : Aesop.MVarCluster) : Aesop.NodeState

Equations

• Aesop.MVarCluster.state c = (Aesop.MVarCluster.elim c).state

@[inline]

def Aesop.MVarCluster.setState (state : Aesop.NodeState) (c : Aesop.MVarCluster) : Aesop.MVarCluster

Equations

• Aesop.MVarCluster.setState state c = Aesop.MVarCluster.modify (fun c => { parent? := c.parent?, goals := c.goals, isIrrelevant := c.isIrrelevant, state := state }) c

@[inline]

def Aesop.Goal.mk : Aesop.GoalData Aesop.Rapp Aesop.MVarCluster → Aesop.Goal

Equations

• Aesop.Goal.mk = Aesop.tree.introGoal

@[inline]

def Aesop.Goal.elim : Aesop.Goal → Aesop.GoalData Aesop.Rapp Aesop.MVarCluster

Equations

• Aesop.Goal.elim = Aesop.tree.elimGoal

@[inline]

def Aesop.Goal.modify (f : Aesop.GoalData Aesop.Rapp Aesop.MVarCluster → Aesop.GoalData Aesop.Rapp Aesop.MVarCluster) (g : Aesop.Goal) : Aesop.Goal

Equations

• Aesop.Goal.modify f g = Aesop.Goal.mk (f (Aesop.Goal.elim g))

@[inline]

def Aesop.Goal.id (g : Aesop.Goal) : Aesop.GoalId

Equations

• Aesop.Goal.id g = (Aesop.Goal.elim g).id

@[inline]

def Aesop.Goal.parent (g : Aesop.Goal) : Aesop.MVarClusterRef

Equations

• Aesop.Goal.parent g = (Aesop.Goal.elim g).parent

@[inline]

def Aesop.Goal.children (g : Aesop.Goal) : Array Aesop.RappRef

Equations

• Aesop.Goal.children g = (Aesop.Goal.elim g).children

@[inline]

def Aesop.Goal.origin (g : Aesop.Goal) : Aesop.GoalOrigin

Equations

• Aesop.Goal.origin g = (Aesop.Goal.elim g).origin

@[inline]

def Aesop.Goal.depth (g : Aesop.Goal) : Nat

Equations

• Aesop.Goal.depth g = (Aesop.Goal.elim g).depth

@[inline]

def Aesop.Goal.state (g : Aesop.Goal) : Aesop.GoalState

Equations

• Aesop.Goal.state g = (Aesop.Goal.elim g).state

@[inline]

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

Equations

• Aesop.Goal.isIrrelevant g = (Aesop.Goal.elim g).isIrrelevant

@[inline]

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

Equations

• Aesop.Goal.isForcedUnprovable g = (Aesop.Goal.elim g).isForcedUnprovable

@[inline]

def Aesop.Goal.preNormGoal (g : Aesop.Goal) : Lean.MVarId

Equations

• Aesop.Goal.preNormGoal g = (Aesop.Goal.elim g).preNormGoal

@[inline]

def Aesop.Goal.normalizationState (g : Aesop.Goal) : Aesop.NormalizationState

Equations

• Aesop.Goal.normalizationState g = (Aesop.Goal.elim g).normalizationState

@[inline]

def Aesop.Goal.mvars (g : Aesop.Goal) : Aesop.UnorderedArraySet Lean.MVarId

Equations

• Aesop.Goal.mvars g = (Aesop.Goal.elim g).mvars

@[inline]

def Aesop.Goal.successProbability (g : Aesop.Goal) : Aesop.Percent

Equations

• Aesop.Goal.successProbability g = (Aesop.Goal.elim g).successProbability

@[inline]

def Aesop.Goal.addedInIteration (g : Aesop.Goal) : Aesop.Iteration

Equations

• Aesop.Goal.addedInIteration g = (Aesop.Goal.elim g).addedInIteration

@[inline]

def Aesop.Goal.lastExpandedInIteration (g : Aesop.Goal) : Aesop.Iteration

Equations

• Aesop.Goal.lastExpandedInIteration g = (Aesop.Goal.elim g).lastExpandedInIteration

@[inline]

def Aesop.Goal.failedRapps (g : Aesop.Goal) : Array Aesop.RegularRule

Equations

• Aesop.Goal.failedRapps g = (Aesop.Goal.elim g).failedRapps

@[inline]

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

Equations

• Aesop.Goal.unsafeRulesSelected g = (Aesop.Goal.elim g).unsafeRulesSelected

@[inline]

def Aesop.Goal.unsafeQueue (g : Aesop.Goal) : Aesop.UnsafeQueue

Equations

• Aesop.Goal.unsafeQueue g = (Aesop.Goal.elim g).unsafeQueue

@[inline]

def Aesop.Goal.unsafeQueue? (g : Aesop.Goal) : Option Aesop.UnsafeQueue

Equations

• Aesop.Goal.unsafeQueue? g = if Aesop.Goal.unsafeRulesSelected g = true then some (Aesop.Goal.unsafeQueue g) else none

@[inline]

def Aesop.Goal.setId (id : Aesop.GoalId) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setParent (parent : Aesop.MVarClusterRef) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setChildren (children : Array Aesop.RappRef) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setOrigin (origin : Aesop.GoalOrigin) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setDepth (depth : Nat) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setIsIrrelevant (isIrrelevant : Bool) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setIsForcedUnprovable (isForcedUnprovable : Bool) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setPreNormGoal (preNormGoal : Lean.MVarId) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setNormalizationState (normalizationState : Aesop.NormalizationState) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setMVars (mvars : Aesop.UnorderedArraySet Lean.MVarId) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setSuccessProbability (successProbability : Aesop.Percent) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setAddedInIteration (addedInIteration : Aesop.Iteration) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setLastExpandedInIteration (lastExpandedInIteration : Aesop.Iteration) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setUnsafeRulesSelected (unsafeRulesSelected : Bool) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setUnsafeQueue (unsafeQueue : Aesop.UnsafeQueue) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setState (state : Aesop.GoalState) (g : Aesop.Goal) : Aesop.Goal

Equations

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

@[inline]

def Aesop.Goal.setFailedRapps (failedRapps : Array Aesop.RegularRule) (g : Aesop.Goal) : Aesop.Goal

Equations

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

instance Aesop.Goal.instNonemptyGoal : Nonempty Aesop.Goal

Equations

• Aesop.Goal.instNonemptyGoal = Aesop.Goal.instNonemptyGoal.proof_1

instance Aesop.Goal.instBEqGoal : BEq Aesop.Goal

Equations

• Aesop.Goal.instBEqGoal = { beq := fun g₁ g₂ => Aesop.Goal.id g₁ == Aesop.Goal.id g₂ }

instance Aesop.Goal.instHashableGoal : Hashable Aesop.Goal

Equations

• Aesop.Goal.instHashableGoal = { hash := fun g => hash (Aesop.Goal.id g) }

@[inline]

def Aesop.Rapp.mk : Aesop.RappData Aesop.Goal Aesop.MVarCluster → Aesop.Rapp

Equations

• Aesop.Rapp.mk = Aesop.tree.introRapp

@[inline]

def Aesop.Rapp.elim : Aesop.Rapp → Aesop.RappData Aesop.Goal Aesop.MVarCluster

Equations

• Aesop.Rapp.elim = Aesop.tree.elimRapp

@[inline]

def Aesop.Rapp.modify (f : Aesop.RappData Aesop.Goal Aesop.MVarCluster → Aesop.RappData Aesop.Goal Aesop.MVarCluster) (r : Aesop.Rapp) : Aesop.Rapp

Equations

• Aesop.Rapp.modify f r = Aesop.Rapp.mk (f (Aesop.Rapp.elim r))

@[inline]

def Aesop.Rapp.id (r : Aesop.Rapp) : Aesop.RappId

Equations

• Aesop.Rapp.id r = (Aesop.Rapp.elim r).id

@[inline]

def Aesop.Rapp.parent (r : Aesop.Rapp) : Aesop.GoalRef

Equations

• Aesop.Rapp.parent r = (Aesop.Rapp.elim r).parent

@[inline]

def Aesop.Rapp.children (r : Aesop.Rapp) : Array Aesop.MVarClusterRef

Equations

• Aesop.Rapp.children r = (Aesop.Rapp.elim r).children

@[inline]

def Aesop.Rapp.state (r : Aesop.Rapp) : Aesop.NodeState

Equations

• Aesop.Rapp.state r = (Aesop.Rapp.elim r).state

@[inline]

def Aesop.Rapp.isIrrelevant (r : Aesop.Rapp) : Bool

Equations

• Aesop.Rapp.isIrrelevant r = (Aesop.Rapp.elim r).isIrrelevant

@[inline]

def Aesop.Rapp.appliedRule (r : Aesop.Rapp) : Aesop.RegularRule

Equations

• Aesop.Rapp.appliedRule r = (Aesop.Rapp.elim r).appliedRule

@[inline]

def Aesop.Rapp.scriptBuilder? (r : Aesop.Rapp) : Option Aesop.RuleTacScriptBuilder

Equations

• Aesop.Rapp.scriptBuilder? r = (Aesop.Rapp.elim r).scriptBuilder?

@[inline]

def Aesop.Rapp.originalSubgoals (r : Aesop.Rapp) : Array Lean.MVarId

Equations

• Aesop.Rapp.originalSubgoals r = (Aesop.Rapp.elim r).originalSubgoals

@[inline]

def Aesop.Rapp.successProbability (r : Aesop.Rapp) : Aesop.Percent

Equations

• Aesop.Rapp.successProbability r = (Aesop.Rapp.elim r).successProbability

@[inline]

def Aesop.Rapp.metaState (r : Aesop.Rapp) : Lean.Meta.SavedState

Equations

• Aesop.Rapp.metaState r = (Aesop.Rapp.elim r).metaState

@[inline]

def Aesop.Rapp.introducedMVars (r : Aesop.Rapp) : Aesop.UnorderedArraySet Lean.MVarId

Equations

• Aesop.Rapp.introducedMVars r = (Aesop.Rapp.elim r).introducedMVars

@[inline]

def Aesop.Rapp.assignedMVars (r : Aesop.Rapp) : Aesop.UnorderedArraySet Lean.MVarId

Equations

• Aesop.Rapp.assignedMVars r = (Aesop.Rapp.elim r).assignedMVars

@[inline]

def Aesop.Rapp.setId (id : Aesop.RappId) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setParent (parent : Aesop.GoalRef) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setChildren (children : Array Aesop.MVarClusterRef) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setState (state : Aesop.NodeState) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setIsIrrelevant (isIrrelevant : Bool) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setAppliedRule (appliedRule : Aesop.RegularRule) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setScriptBuilder? (scriptBuilder? : Option Aesop.RuleTacScriptBuilder) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setOriginalSubgoals (originalSubgoals : Array Lean.MVarId) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setSuccessProbability (successProbability : Aesop.Percent) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setMetaState (metaState : Lean.Meta.SavedState) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setIntroducedMVars (introducedMVars : Aesop.UnorderedArraySet Lean.MVarId) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

@[inline]

def Aesop.Rapp.setAssignedMVars (assignedMVars : Aesop.UnorderedArraySet Lean.MVarId) (r : Aesop.Rapp) : Aesop.Rapp

Equations

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

instance Aesop.Rapp.instNonemptyRapp : Nonempty Aesop.Rapp

Equations

• Aesop.Rapp.instNonemptyRapp = Aesop.Rapp.instNonemptyRapp.proof_1

instance Aesop.Rapp.instBEqRapp : BEq Aesop.Rapp

Equations

• Aesop.Rapp.instBEqRapp = { beq := fun r₁ r₂ => Aesop.Rapp.id r₁ == Aesop.Rapp.id r₂ }

instance Aesop.Rapp.instHashableRapp : Hashable Aesop.Rapp

Equations

• Aesop.Rapp.instHashableRapp = { hash := fun r => hash (Aesop.Rapp.id r) }

Miscellaneous Queries

@[inline]

def Aesop.Goal.postNormGoalAndMetaState? (g : Aesop.Goal) : Option (Lean.MVarId × Lean.Meta.SavedState)

Equations

• Aesop.Goal.postNormGoalAndMetaState? g = match Aesop.Goal.normalizationState g with | Aesop.NormalizationState.normal postGoal postState script? => some (postGoal, postState) | x => none

def Aesop.Goal.postNormGoal? (g : Aesop.Goal) : Option Lean.MVarId

Equations

• Aesop.Goal.postNormGoal? g = Option.map (fun x => x.fst) (Aesop.Goal.postNormGoalAndMetaState? g)

def Aesop.Goal.currentGoal (g : Aesop.Goal) : Lean.MVarId

Equations

• Aesop.Goal.currentGoal g = Option.getD (Aesop.Goal.postNormGoal? g) (Aesop.Goal.preNormGoal g)

def Aesop.Goal.parentRapp? (g : Aesop.Goal) : BaseIO (Option Aesop.RappRef)

Equations

• Aesop.Goal.parentRapp? g = do let __do_lift ← ST.Ref.get (Aesop.Goal.parent g) pure (Aesop.MVarCluster.parent? __do_lift)

def Aesop.Goal.parentMetaState (g : Aesop.Goal) (rootMetaState : Lean.Meta.SavedState) : BaseIO Lean.Meta.SavedState

Equations

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

def Aesop.Goal.currentGoalAndMetaState (g : Aesop.Goal) (rootMetaState : Lean.Meta.SavedState) : Lean.MetaM (Lean.MVarId × Lean.Meta.SavedState)

Equations

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

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

Equations

• Aesop.Goal.isUnsafeExhausted g = (Aesop.Goal.unsafeRulesSelected g && Subarray.isEmpty (Aesop.Goal.unsafeQueue g))

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

Equations

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

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

Equations

• Aesop.Goal.isActive g = do let __do_lift ← pure (Aesop.Goal.isIrrelevant g) <||> Aesop.Goal.isExhausted g pure !__do_lift

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

Equations

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

def Aesop.Goal.firstProvenRapp? (g : Aesop.Goal) : BaseIO (Option Aesop.RappRef)

Equations

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

def Aesop.Goal.safeRapps (g : Aesop.Goal) : BaseIO (Array Aesop.RappRef)

Equations

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

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

Equations

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

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

Equations

• Aesop.Goal.hasMVar g = !Aesop.UnorderedArraySet.isEmpty (Aesop.Goal.mvars g)

def Aesop.Goal.priority (g : Aesop.Goal) : Aesop.Percent

Equations

• Aesop.Goal.priority g = Aesop.Goal.successProbability g * Aesop.unificationGoalPenalty ^ Aesop.UnorderedArraySet.size (Aesop.Goal.mvars g)

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

Equations

• Aesop.Goal.isNormal g = Aesop.NormalizationState.isNormal (Aesop.Goal.normalizationState g)

def Aesop.Goal.originalGoalId (g : Aesop.Goal) : Aesop.GoalId

Equations

• Aesop.Goal.originalGoalId g = Option.getD (Aesop.GoalOrigin.originalGoalId? (Aesop.Goal.origin g)) (Aesop.Goal.id g)

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

Equations

• Aesop.Goal.isRoot g = do let __do_lift ← Aesop.Goal.parentRapp? g pure (Option.isNone __do_lift)

def Aesop.Rapp.introducesMVar (r : Aesop.Rapp) : Bool

Equations

• Aesop.Rapp.introducesMVar r = !Aesop.UnorderedArraySet.isEmpty (Aesop.Rapp.introducedMVars r)

def Aesop.Rapp.parentPostNormMetaState (r : Aesop.Rapp) (rootMetaState : Lean.Meta.SavedState) : BaseIO Lean.Meta.SavedState

Equations

• Aesop.Rapp.parentPostNormMetaState r rootMetaState = do let __do_lift ← ST.Ref.get (Aesop.Rapp.parent r) Aesop.Goal.parentMetaState __do_lift rootMetaState

def Aesop.Rapp.foldSubgoalsM {m : Type → Type} {σ : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (init : σ) (f : σ → Aesop.GoalRef → m σ) (r : Aesop.Rapp) : m σ

Equations

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

def Aesop.Rapp.forSubgoalsM {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (f : Aesop.GoalRef → m Unit) (r : Aesop.Rapp) : m Unit

Equations

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

def Aesop.Rapp.subgoals {m : Type → Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (r : Aesop.Rapp) : m (Array Aesop.GoalRef)

Equations

• Aesop.Rapp.subgoals r = Aesop.Rapp.foldSubgoalsM #[] (fun subgoals gref => pure (Array.push subgoals gref)) r

def Aesop.Rapp.depth (r : Aesop.Rapp) : BaseIO Nat

Equations

• Aesop.Rapp.depth r = do let __do_lift ← ST.Ref.get (Aesop.Rapp.parent r) pure (Aesop.Goal.depth __do_lift)

def Aesop.MVarCluster.provenGoal? (c : Aesop.MVarCluster) : BaseIO (Option Aesop.GoalRef)

Equations

• Aesop.MVarCluster.provenGoal? c = Array.findM? (Aesop.MVarCluster.goals c) fun gref => do let __do_lift ← ST.Ref.get gref pure (Aesop.GoalState.isProven (Aesop.Goal.state __do_lift))