inductive Aesop.Script.SScript : Type

• empty: Aesop.Script.SScript
• onGoal: Nat → Aesop.Script.Step → Aesop.Script.SScript → Aesop.Script.SScript
• focusAndSolve: Nat → Aesop.Script.SScript → Aesop.Script.SScript → Aesop.Script.SScript

instance Aesop.Script.instInhabitedSScript : Inhabited Aesop.Script.SScript

Equations

• Aesop.Script.instInhabitedSScript = { default := Aesop.Script.SScript.empty }

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

Equations

• Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? acc 0 x = some (acc, x)
• Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? acc n.succ Aesop.Script.SScript.empty = none
• Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? acc n.succ (Aesop.Script.SScript.onGoal goalPos step tail) = none
• Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? acc n.succ (Aesop.Script.SScript.focusAndSolve 0 here tail) = Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? (acc.push here) n tail
• Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? acc n.succ (Aesop.Script.SScript.focusAndSolve n_1.succ here tail) = none

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

Equations

• script.render = Aesop.Script.SScript.render.go #[] script

partial def Aesop.Script.SScript.render.go {m : Type → Type} [Monad m] [Lean.MonadError m] [Lean.MonadQuotation m] (acc : Array Lean.Syntax.Tactic) : Aesop.Script.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 : Aesop.Script.Step) (tail : Aesop.Script.SScript) : m (Option (Lean.Syntax.Tactic × Aesop.Script.SScript))