def Aesop.isForwardOrDestructRuleName (n : Aesop.RuleName) : Bool

Equations

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

structure Aesop.SaturateM.Context : Type

• options : Aesop.Options'

@[reducible, inline]

abbrev Aesop.SaturateM (α : Type) : Type

Equations

• Aesop.SaturateM = ReaderT Aesop.SaturateM.Context Lean.MetaM

def Aesop.getSingleGoal {m : Type → Type} [Monad m] [Lean.MonadError m] (o : Aesop.RuleTacOutput) : m (Lean.MVarId × Lean.Meta.SavedState)

Equations

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

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

Equations

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

partial def Aesop.saturate.go (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) : Aesop.SaturateM Lean.MVarId

def Aesop.saturate.runRule {α : Type} (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId) (preState : Lean.Meta.SavedState) (matchResult : Aesop.IndexMatchResult (Aesop.Rule α)) : Aesop.SaturateM (Option Lean.MVarId)

Equations

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

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

Equations

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