@[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 : UTactic
• sTactic? : Option STactic

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

Equations

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

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

Equations

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

def Aesop.Script.Tactic.structured (uTactic : UTactic) (sTactic : STactic) : 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