source
@[reducible, inline]
abbrev Aesop.Script.UTactic :
Type
Equations

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

Instances For

source
structure Aesop.Script.STactic :
Type

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

Instances For

source
structure Aesop.Script.Tactic :
Type

- uTactic : UTactic
- sTactic? : Option STactic

Instances For

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

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

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

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

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Aesop.Script.TacticBuilder :
Type
Equations

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

Instances For