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 }

structure Aesop.SaturateM.State : Type

• rulePatternCache : RulePatternCache
• rpinfCache : RPINFCache

instance Aesop.SaturateM.instInhabitedState : Inhabited State

Equations

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

def Aesop.SaturateM.instInhabitedState.default : 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.

@[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.

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.