structure Aesop.Tree : Type

• root : MVarClusterRef
• rootMetaState : Lean.Meta.SavedState
• numGoals : Nat
• numRapps : Nat
• nextGoalId : GoalId
• nextRappId : RappId
• allIntroducedMVars : Std.HashSet Lean.MVarId

  Union of the mvars introduced by all rapps.

def Aesop.mkInitialTree (goal : Lean.MVarId) (rs : LocalRuleSet) : BaseM Tree

Equations

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

structure Aesop.TreeM.Context : Type

• currentIteration : Iteration
• ruleSet : LocalRuleSet

structure Aesop.TreeM.State : Type

• tree : Tree

@[reducible, inline]

abbrev Aesop.TreeM (α : Type) : Type

Equations

• Aesop.TreeM = ReaderT Aesop.TreeM.Context (StateRefT' IO.RealWorld Aesop.TreeM.State Aesop.BaseM)

instance Aesop.TreeM.instMonad : Monad TreeM

Equations

• Aesop.TreeM.instMonad = inferInstanceAs (Monad Aesop.TreeM)

@[instance 100]

instance Aesop.TreeM.instMonadStateOfTree : MonadStateOf Tree TreeM

Equations

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

instance Aesop.TreeM.instInhabited {α : Type} : Inhabited (TreeM α)

Equations

• Aesop.TreeM.instInhabited = { default := failure }

def Aesop.TreeM.run' {α : Type} (ctx : Context) (tree : Tree) (x : TreeM α) : BaseM (α × State)

Equations

• Aesop.TreeM.run' ctx tree x = (ReaderT.run x ctx).run { tree := tree }

def Aesop.getRootMVarCluster : TreeM MVarClusterRef

Equations

• Aesop.getRootMVarCluster = do let __do_lift ← getThe Aesop.Tree pure __do_lift.root

def Aesop.getRootMetaState : TreeM Lean.Meta.SavedState

Equations

• Aesop.getRootMetaState = do let __do_lift ← getThe Aesop.Tree pure __do_lift.rootMetaState

def Aesop.getRootGoal : TreeM GoalRef

Equations

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

def Aesop.getRootMVarId : TreeM Lean.MVarId

Equations

• Aesop.getRootMVarId = do let gref ← Aesop.getRootGoal let __do_lift ← ST.Ref.get gref pure __do_lift.preNormGoal

def Aesop.incrementNumGoals (increment : Nat := 1) : TreeM Unit

Equations

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

def Aesop.incrementNumRapps (increment : Nat := 1) : TreeM Unit

Equations

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

def Aesop.getAllIntroducedMVars : TreeM (Std.HashSet Lean.MVarId)

Equations

• Aesop.getAllIntroducedMVars = do let __do_lift ← getThe Aesop.Tree pure __do_lift.allIntroducedMVars

def Aesop.getAndIncrementNextGoalId : TreeM GoalId

Equations

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

def Aesop.getAndIncrementNextRappId : TreeM RappId

Equations

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