@[reducible, inline]

abbrev Aesop.Script.UTactic : Type

Equations

• Aesop.Script.UTactic = Lean.Syntax.Tactic

structure Aesop.Script.STactic : Type

• numSubgoals : Nat
• run : Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic

structure Aesop.Script.Tactic : Type

• uTactic : Aesop.Script.UTactic
• sTactic? : Option Aesop.Script.STactic

Instances For

• Aesop.Script.Tactic.instToMessageData

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

Equations

• Aesop.Script.Tactic.instToMessageData = { toMessageData := fun (t : Aesop.Script.Tactic) => Lean.toMessageData t.uTactic }

def Aesop.Script.Tactic.unstructured (uTactic : Aesop.Script.UTactic) : Aesop.Script.Tactic

Equations

• Aesop.Script.Tactic.unstructured uTactic = { uTactic := uTactic, sTactic? := none }

def Aesop.Script.Tactic.structured (uTactic : Aesop.Script.UTactic) (sTactic : Aesop.Script.STactic) : Aesop.Script.Tactic

Equations

• Aesop.Script.Tactic.structured uTactic sTactic = { uTactic := uTactic, sTactic? := some sTactic }

@[reducible, inline]

abbrev Aesop.Script.TacticBuilder : Type

Equations

• Aesop.Script.TacticBuilder = Lean.MetaM Aesop.Script.Tactic