source
inductive Aesop.Script.SScript :
Type

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

Instances For

source
instance Aesop.Script.instInhabitedSScript :
Inhabited SScript
Equations

- Aesop.Script.instInhabitedSScript = { default := Aesop.Script.instInhabitedSScript.default }

source
def Aesop.Script.instInhabitedSScript.default :
SScript
Equations

- Aesop.Script.instInhabitedSScript.default = Aesop.Script.SScript.empty

Instances For

source
def Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? (acc : Array SScript) :
Nat → SScript → Option (Array SScript × 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

Instances For

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

- script.render = Aesop.Script.SScript.render.go✝ #[] script

Instances For