@[inline]

def Aesop.Script.mkOneBasedNumLit (n : Nat) : Lean.NumLit

Equations

• Aesop.Script.mkOneBasedNumLit n = Lean.Syntax.mkNumLit (toString (n + 1))

def Aesop.Script.mkOnGoal (goalPos : Nat) (tac : Lean.Syntax.Tactic) : Lean.Syntax.Tactic

Equations

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

structure Aesop.Script.Step : Type

• preState : Lean.Meta.SavedState
• preGoal : Lean.MVarId
• tactic : Aesop.Script.Tactic
• postState : Lean.Meta.SavedState
• postGoals : Array Aesop.GoalWithMVars

def Aesop.Script.TacticState.applyStep {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : Aesop.Script.TacticState) (step : Aesop.Script.Step) : m Aesop.Script.TacticState

Equations

• tacticState.applyStep step = tacticState.applyTactic step.preGoal step.postGoals step.preState.meta.mctx step.postState.meta.mctx

def Aesop.Script.Step.uTactic (s : Aesop.Script.Step) : Aesop.Script.UTactic

Equations

• s.uTactic = s.tactic.uTactic

def Aesop.Script.Step.sTactic? (s : Aesop.Script.Step) : Option Aesop.Script.STactic

Equations

• s.sTactic? = s.tactic.sTactic?

instance Aesop.Script.Step.instToMessageData : Lean.ToMessageData Aesop.Script.Step

Equations

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

def Aesop.Script.Step.mkSorry (preGoal : Lean.MVarId) (preState : Lean.Meta.SavedState) : Lean.MetaM Aesop.Script.Step

Equations

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

def Aesop.Script.Step.render {m : Type → Type} [Monad m] [Lean.MonadError m] (acc : Array Lean.Syntax.Tactic) (step : Aesop.Script.Step) (tacticState : Aesop.Script.TacticState) : m (Array Lean.Syntax.Tactic × Aesop.Script.TacticState)

Equations

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

def Aesop.Script.Step.validate (step : Aesop.Script.Step) : Lean.MetaM Unit

Equations

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

def Aesop.Script.Step.validate.fmtGoals (state : Lean.Meta.SavedState) (goals : Array Lean.MVarId) : Lean.MetaM Lean.MessageData

Equations

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

structure Aesop.Script.LazyStep : Type

• preState : Lean.Meta.SavedState
• preGoal : Lean.MVarId
• tacticBuilder : Aesop.Script.TacticBuilder
• postState : Lean.Meta.SavedState
• postGoals : Array Lean.MVarId

def Aesop.Script.LazyStep.toStep (s : Aesop.Script.LazyStep) : Lean.MetaM Aesop.Script.Step

Equations

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

structure Aesop.Script.LazyStep.BuildInput (α : Type) : Type

• tac : Lean.MetaM α
• postGoals : α → Array Lean.MVarId
• tacticBuilder : α → Aesop.Script.TacticBuilder

@[always_inline]

def Aesop.Script.LazyStep.build {α : Type} (preGoal : Lean.MVarId) (i : Aesop.Script.LazyStep.BuildInput α) : Lean.MetaM (Aesop.Script.LazyStep × α)

Equations

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

def Aesop.Script.LazyStep.erasePostStateAssignments (s : Aesop.Script.LazyStep) (gs : Array Lean.MVarId) : Aesop.Script.LazyStep

Equations

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