source
@[inline]
def Aesop.Script.mkOneBasedNumLit (n : Nat) :
Lean.NumLit
Equations

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

Instances For

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

Instances For

source
structure Aesop.Script.Step :
Type

- preState : Lean.Meta.SavedState
- preGoal : Lean.MVarId
- tactic : Tactic
- postState : Lean.Meta.SavedState
- postGoals : Array GoalWithMVars

Instances For

source
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

Instances For

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

- s.uTactic = s.tactic.uTactic

Instances For

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

- s.sTactic? = s.tactic.sTactic?

Instances For

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

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

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

Instances For

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

- tac : Lean.MetaM α
- postGoals : α → Array Lean.MVarId
- tacticBuilder : α → TacticBuilder

Instances For

source
@[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.

Instances For

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

Instances For