structure Aesop.BaseM.State : Type

State of the BaseM monad.

• rulePatternCache : RulePatternCache

  The rule pattern cache.

• rpinfCache : RPINFCache

  The RPINF cache.

• stats : Stats

  Stats collected during an Aesop call.

instance Aesop.BaseM.instInhabitedState : Inhabited State

instance Aesop.instEmptyCollectionState : EmptyCollection BaseM.State

@[reducible, inline]

abbrev Aesop.BaseM (α : Type) : Type

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

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

Run a BaseM action.

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

instance Aesop.BaseM.instMonadHashMapCacheAdapterExprRPINFRaw : Lean.MonadHashMapCacheAdapter Lean.Expr RPINFRaw BaseM

instance Aesop.BaseM.instMonadStats : MonadStats BaseM

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