inductive Aesop.Script.SScript : Type

• empty : SScript
• onGoal (goalPos : Nat) (step : Step) (tail : SScript) : SScript
• focusAndSolve (goalPos : Nat) (here tail : SScript) : SScript

instance Aesop.Script.instInhabitedSScript : Inhabited SScript

def Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? (acc : Array SScript) : Nat → SScript → Option (Array SScript × SScript)

def Aesop.Script.SScript.render {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (script : SScript) : m (Array Lean.Syntax.Tactic)

partial def Aesop.Script.SScript.render.go {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (acc : Array Lean.Syntax.Tactic) : SScript → m (Array Lean.Syntax.Tactic)

partial def Aesop.Script.SScript.render.renderSTactic? {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (goalPos : Nat) (step : Step) (tail : SScript) : m (Option (Lean.Syntax.Tactic × SScript))