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'

def Aesop.SaturateM.instInhabitedContext.default : Context

Equations

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

instance Aesop.SaturateM.instInhabitedContext : Inhabited Context

Equations

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

@[reducible, inline]

abbrev Aesop.SaturateM (α : Type) : Type

Equations

• Aesop.SaturateM = ReaderT Aesop.SaturateM.Context (Aesop.ScriptT Aesop.BaseM)

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

Equations

• Aesop.SaturateM.run options x = do let __discr ← (ReaderT.run x { options := options }).run.run match __discr with | ((a, snd), stats) => pure (a, stats)

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.

@[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) : SaturateM Lean.MVarId

Equations

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

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

Equations

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

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

Equations

• Aesop.saturateMain rs goal = do let goal ← Aesop.saturateMain' rs goal let __do_lift ← Aesop.getStats liftM (__do_lift.trace Aesop.TraceOption.stats) pure goal

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

Equations

• Aesop.saturate rs goal options = Aesop.SaturateM.run options (Aesop.saturateMain rs goal)