def Aesop.isForwardOrDestructRuleName (n : RuleName) : Bool

structure Aesop.SaturateM.Context : Type

• options : Options'

instance Aesop.SaturateM.instInhabitedContext : Inhabited Context

structure Aesop.SaturateM.State : Type

• rulePatternCache : RulePatternCache
• rpinfCache : RPINFCache

instance Aesop.SaturateM.instInhabitedState : Inhabited State

@[reducible, inline]

abbrev Aesop.SaturateM (α : Type) : Type

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

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

partial def Aesop.saturateCore.go (rs : LocalRuleSet) (goal : Lean.MVarId) (fs : ForwardState) : SaturateM Lean.MVarId

def Aesop.saturateCore.tryNormRules (rs : LocalRuleSet) (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (hypTypes : Lean.PHashSet RPINF) : SaturateM (Option GoalDiff)

def Aesop.saturateCore.trySafeRules (rs : LocalRuleSet) (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (hypTypes : Lean.PHashSet RPINF) : SaturateM (Option GoalDiff)

def Aesop.saturateCore.runRule {α : Type} (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (matchResult : IndexMatchResult (Rule α)) (hypTypes : Lean.PHashSet RPINF) : SaturateM (Option (GoalDiff × Option (Array Script.LazyStep)))

def Aesop.saturateCore.runFirstRule {α : Type} (goal : Lean.MVarId) (mvars : UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (matchResults : Array (IndexMatchResult (Rule α))) (hypTypes : Lean.PHashSet RPINF) : SaturateM (Option GoalDiff)

@[reducible, inline]

abbrev Aesop.Stateful.Queue : Type

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

partial def Aesop.Stateful.saturateCore.go (rs : LocalRuleSet) (options : Options') (hypDepths : Std.HashMap Lean.FVarId Nat) (fs : ForwardState) (queue : Queue) (erasedHyps : Std.HashSet Lean.FVarId) (goal : Lean.MVarId) : SaturateM Lean.MVarId

def Aesop.saturateMain (rs : LocalRuleSet) (goal : Lean.MVarId) (options : Options') : Lean.MetaM (Lean.MVarId × Array Script.LazyStep)

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