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) : Lean.MetaM Tree

Equations

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

structure Aesop.TreeM.Context : Type

• currentIteration : Iteration

@[reducible, inline]

abbrev Aesop.TreeM (α : Type) : Type

Equations

• Aesop.TreeM = ReaderT Aesop.TreeM.Context (StateRefT' IO.RealWorld Aesop.Tree Lean.MetaM)

instance Aesop.TreeM.instMonad : Monad TreeM

Equations

• Aesop.TreeM.instMonad = Monad.mk

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

Equations

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

def Aesop.TreeM.run' {α : Type} (ctx : Context) (t : Tree) (x : TreeM α) : Lean.MetaM (α × Tree)

Equations

• Aesop.TreeM.run' ctx t x = (ReaderT.run x ctx).run t

def Aesop.getRootMVarCluster : TreeM MVarClusterRef

Equations

• Aesop.getRootMVarCluster = do let __do_lift ← get pure __do_lift.root

def Aesop.getRootMetaState : TreeM Lean.Meta.SavedState

Equations

• Aesop.getRootMetaState = do let __do_lift ← get 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 ← get 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.