@[reducible, inline]

abbrev Aesop.ScriptT (m : Type → Type) (α : Type) : Type

Equations

• Aesop.ScriptT m = StateRefT' IO.RealWorld (Array Aesop.Script.LazyStep) m

def Aesop.ScriptT.run {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (x : ScriptT m α) : m (α × Array Script.LazyStep)

Equations

• x.run = StateRefT'.run x #[]

@[reducible, inline]

abbrev Aesop.ScriptM (α : Type) : Type

Equations

• Aesop.ScriptM = Aesop.ScriptT Lean.MetaM

def Aesop.recordScriptStep {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (step : Script.LazyStep) : m Unit

Equations

• Aesop.recordScriptStep step = modify fun (x : Array Aesop.Script.LazyStep) => x.push step

def Aesop.recordScriptSteps {m : Type → Type u_1} [MonadStateOf (Array Script.LazyStep) m] (steps : Array Script.LazyStep) : m Unit

Equations

• Aesop.recordScriptSteps steps = modify fun (x : Array Aesop.Script.LazyStep) => x ++ steps

def Aesop.withScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (success : α → Bool) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM α) : ScriptM α

Equations

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

def Aesop.withOptScriptStep {α : Type} (preGoal : Lean.MVarId) (postGoals : α → Array Lean.MVarId) (tacticBuilder : α → Script.TacticBuilder) (x : Lean.MetaM (Option α)) : ScriptM (Option α)

Equations

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