@[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
• tacticBuilders : Array Aesop.Script.TacticBuilder

  A nonempty list of tactic builders. During script generation, Aesop tries to execute the builders from left to right. It then uses the first builder that succceds (in the sense that when run in preState on preGoal it produces the postState and postGoals). The last builder must succeed and is used unconditionally.

• tacticBuilders_ne : 0 < self.tacticBuilders.size
• postState : Lean.Meta.SavedState
• postGoals : Array Lean.MVarId

theorem Aesop.Script.LazyStep.tacticBuilders_ne (self : Aesop.Script.LazyStep) : 0 < self.tacticBuilders.size

def Aesop.Script.LazyStep.runFirstSuccessfulTacticBuilder (s : Aesop.Script.LazyStep) : Lean.MetaM Aesop.Script.Tactic

Equations

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

def Aesop.Script.LazyStep.runFirstSuccessfulTacticBuilder.tryTacticBuilder (s : Aesop.Script.LazyStep) (b : Aesop.Script.TacticBuilder) : Lean.MetaM (Option Aesop.Script.Tactic)

Equations

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

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.