@[inline]

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

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

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

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

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

@[implicit_reducible]

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

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

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)

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

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

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

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 × α)

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