def Aesop.isForwardOrDestructRuleName (n : RuleName) : Bool

structure Aesop.SaturateM.Context : Type

• options : Options'

def Aesop.SaturateM.instInhabitedContext.default : Context

@[implicit_reducible]

instance Aesop.SaturateM.instInhabitedContext : Inhabited Context

@[reducible, inline]

abbrev Aesop.SaturateM (α : Type) : Type

def Aesop.SaturateM.run {α : Type} (options : Options') (x : SaturateM α) : Lean.MetaM (α × Stats)

def Aesop.getSingleGoal {m : Type → Type} [Monad m] [Lean.MonadError m] (o : RuleTacOutput) : m (GoalDiff × Lean.Meta.SavedState × Option (Array Script.LazyStep))

def Aesop.saturateCore (rs : LocalRuleSet) (goal : Lean.MVarId) : SaturateM Lean.MVarId

@[reducible, inline]

abbrev Aesop.Stateful.Queue : Type

def Aesop.Stateful.saturateCore (rs : LocalRuleSet) (goal : Lean.MVarId) : SaturateM Lean.MVarId

def Aesop.saturateMain' (rs : LocalRuleSet) (goal : Lean.MVarId) : SaturateM Lean.MVarId

def Aesop.saturateMain (rs : LocalRuleSet) (goal : Lean.MVarId) : SaturateM Lean.MVarId

def Aesop.saturate (rs : LocalRuleSet) (goal : Lean.MVarId) (options : Options') : Lean.MetaM (Lean.MVarId × Stats)