@[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 : Tactic
• postState : Lean.Meta.SavedState
• postGoals : Array GoalWithMVars

def Aesop.Script.TacticState.applyStep {m : Type → Type} [Monad m] [Lean.MonadError m] (tacticState : TacticState) (step : Step) : m 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 : Step) : UTactic

Equations

• s.uTactic = s.tactic.uTactic

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

Equations

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

instance Aesop.Script.Step.instToMessageData : Lean.ToMessageData 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 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 : Step) (tacticState : TacticState) : m (Array Lean.Syntax.Tactic × TacticState)

Equations

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

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

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 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

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

Equations

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

def Aesop.Script.LazyStep.toStep (s : LazyStep) : Lean.MetaM 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 : α → TacticBuilder

@[always_inline]

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

Equations

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

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

Equations

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