structure Aesop.Tree : Type

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

  Union of the mvars introduced by all rapps.

def Aesop.mkInitialTree (goal : Lean.MVarId) : Lean.MetaM Aesop.Tree

Equations

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

structure Aesop.TreeM.Context : Type

• currentIteration : Aesop.Iteration

@[inline, reducible]

abbrev Aesop.TreeM (α : Type) : Type

Equations

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

instance Aesop.TreeM.instMonadTreeM : Monad Aesop.TreeM

Equations

• Aesop.TreeM.instMonadTreeM = let src := inferInstanceAs (Monad Aesop.TreeM); Monad.mk

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

Equations

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

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

Equations

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

def Aesop.getRootMVarCluster : Aesop.TreeM Aesop.MVarClusterRef

Equations

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

def Aesop.getRootMetaState : Aesop.TreeM Lean.Meta.SavedState

Equations

• Aesop.getRootMetaState = do let __do_lift ← get pure __do_lift.rootMetaState

def Aesop.getRootGoal : Aesop.TreeM Aesop.GoalRef

Equations

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

def Aesop.getRootMVarId : Aesop.TreeM Lean.MVarId

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Aesop.getAllIntroducedMVars = do let __do_lift ← get pure __do_lift.allIntroducedMVars

def Aesop.getAndIncrementNextGoalId : Aesop.TreeM Aesop.GoalId

Equations

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

def Aesop.getAndIncrementNextRappId : Aesop.TreeM Aesop.RappId

Equations

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