def Aesop.isForwardOrDestructRuleName (n : RuleName) : Bool

Equations

• Aesop.isForwardOrDestructRuleName n = (n.builder == Aesop.BuilderName.forward || n.builder == Aesop.BuilderName.destruct)

structure Aesop.SaturateM.Context : Type

• options : Options'

instance Aesop.SaturateM.instInhabitedContext : Inhabited Context

Equations

• Aesop.SaturateM.instInhabitedContext = { default := { options := default } }

structure Aesop.SaturateM.State : Type

• rulePatternCache : RulePatternCache
• rpinfCache : RPINFCache

instance Aesop.SaturateM.instInhabitedState : Inhabited State

Equations

• Aesop.SaturateM.instInhabitedState = { default := { rulePatternCache := default, rpinfCache := default } }

@[reducible, inline]

abbrev Aesop.SaturateM (α : Type) : Type

Equations

• Aesop.SaturateM = ReaderT Aesop.SaturateM.Context (StateRefT' IO.RealWorld Aesop.SaturateM.State (Aesop.ScriptT Aesop.BaseM))

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

Equations

• Aesop.SaturateM.run options x = (fun (x : (α × Array Aesop.Script.LazyStep) × Aesop.Stats) => x.fst) <$> ((ReaderT.run x { options := options }).run' { }).run.run

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

Equations

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

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

Equations

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

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)

Equations

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

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

Equations

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

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)))

Equations

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

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)

Equations

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

@[reducible, inline]

abbrev Aesop.Stateful.Queue : Type

Equations

• Aesop.Stateful.Queue = Batteries.BinomialHeap Aesop.ForwardRuleMatch Aesop.ForwardRuleMatch.le

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

Equations

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

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)

Equations

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

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

Equations

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