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

structure Aesop.TreeM.Context : Type

• currentIteration : Iteration
• ruleSet : LocalRuleSet

structure Aesop.TreeM.State : Type

• tree : Tree

@[reducible, inline]

abbrev Aesop.TreeM (α : Type) : Type

@[implicit_reducible]

instance Aesop.TreeM.instMonad : Monad TreeM

@[implicit_reducible, instance 100]

instance Aesop.TreeM.instMonadStateOfTree : MonadStateOf Tree TreeM

@[implicit_reducible]

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

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

def Aesop.getRootMVarCluster : TreeM MVarClusterRef

def Aesop.getRootMetaState : TreeM Lean.Meta.SavedState

def Aesop.getRootGoal : TreeM GoalRef

def Aesop.getRootMVarId : TreeM Lean.MVarId

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

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

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

def Aesop.getAndIncrementNextGoalId : TreeM GoalId

def Aesop.getAndIncrementNextRappId : TreeM RappId