source
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.

Instances For

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

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

Instances For

source
structure Aesop.TreeM.Context :
Type

- currentIteration : Iteration
- ruleSet : LocalRuleSet

Instances For

source
structure Aesop.TreeM.State :
Type

- tree : Tree

Instances For

source
@[reducible, inline]
abbrev Aesop.TreeM (α : Type) :
Type
Equations

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

Instances For

source
instance Aesop.TreeM.instMonad :
Monad TreeM
Equations

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

source
@[instance 100]
instance Aesop.TreeM.instMonadStateOfTree :
MonadStateOf Tree TreeM
Equations

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

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

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

source
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 }

Instances For

source
def Aesop.getRootMVarCluster :
TreeM MVarClusterRef
Equations

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

Instances For

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

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

Instances For

source
def Aesop.getRootGoal :
TreeM GoalRef
Equations

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Aesop.getAndIncrementNextGoalId :
TreeM GoalId
Equations

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

Instances For

source
def Aesop.getAndIncrementNextRappId :
TreeM RappId
Equations

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

Instances For