Documentation

Aesop.Tree.TreeM

structure Aesop.Tree :

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 :

currentIteration : Aesop.Iteration

@[reducible, inline]

abbrev Aesop.TreeM (α : Type) :

Equations

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

Instances For

instance Aesop.TreeM.instMonad :

Monad Aesop.TreeM

Equations

Aesop.TreeM.instMonad = let __src := inferInstanceAs (Monad Aesop.TreeM); Monad.mk

instance Aesop.TreeM.instInhabited {α : Type} :

Inhabited (Aesop.TreeM α)

Equations

Aesop.TreeM.instInhabited = { 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 = (ReaderT.run x ctx).run 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 __do_lift.preNormGoal

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.