@[reducible, inline]

abbrev Aesop.Script.UScript : Type

Equations

• Aesop.Script.UScript = Array Aesop.Script.Step

def Aesop.Script.UScript.render {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : Aesop.Script.TacticState) (s : Aesop.Script.UScript) : m (Array Lean.Syntax.Tactic)

Equations

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

def Aesop.Script.UScript.renderTacticSeq (uscript : Aesop.Script.UScript) (preState : Lean.Meta.SavedState) (goal : Lean.MVarId) : Lean.MetaM (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Equations

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

def Aesop.Script.UScript.validate (s : Aesop.Script.UScript) : Lean.MetaM Unit

Equations

• s.validate = Array.forM (fun (x : Aesop.Script.Step) => x.validate) s