structure Aesop.BaseM.State : Type

State of the BaseM monad.

• rulePatternCache : RulePatternCache

  The rule pattern cache.

• stats : Stats

  Stats collected during an Aesop call.

def Aesop.BaseM.instInhabitedState.default : State

Equations

• Aesop.BaseM.instInhabitedState.default = { rulePatternCache := default, stats := default }

@[implicit_reducible]

instance Aesop.BaseM.instInhabitedState : Inhabited State

Equations

• Aesop.BaseM.instInhabitedState = { default := Aesop.BaseM.instInhabitedState.default }

@[implicit_reducible]

instance Aesop.instEmptyCollectionState : EmptyCollection BaseM.State

Equations

• Aesop.instEmptyCollectionState = { emptyCollection := { rulePatternCache := ∅, stats := ∅ } }

@[reducible, inline]

abbrev Aesop.BaseM (α : Type) : Type

Aesop's base monad. Contains no interesting data, only various caches and stats.

Equations

• Aesop.BaseM = StateRefT' IO.RealWorld Aesop.BaseM.State Lean.MetaM

def Aesop.BaseM.run {α : Type} (x : BaseM α) (stats : Stats := ∅) : Lean.MetaM (α × Stats)

Run a BaseM action.

Equations

• x.run stats = do let __discr ← StateRefT'.run x { rulePatternCache := ∅, stats := stats } match __discr with | (a, s) => pure (a, s.stats)

@[implicit_reducible]

instance Aesop.BaseM.instMonadHashMapCacheAdapterExprEntry : Lean.MonadHashMapCacheAdapter Lean.Expr RulePatternCache.Entry BaseM

Equations

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

@[implicit_reducible]

instance Aesop.BaseM.instMonadStats : MonadStats BaseM

Equations

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

@[implicit_reducible]

instance Aesop.BaseM.instMonadBacktrackSavedState : Lean.MonadBacktrack Lean.Meta.SavedState BaseM

Equations

• Aesop.BaseM.instMonadBacktrackSavedState = { saveState := liftM Lean.Meta.saveState, restoreState := fun (x : Lean.Meta.SavedState) => liftM x.restore }