Documentation

Aesop.Script.Tactic

source
@[reducible, inline]
abbrev Aesop.Script.UTactic :
Type
Instances For
    source
    structure Aesop.Script.STactic :
    Type
    Instances For
      source
      structure Aesop.Script.Tactic :
      Type
      Instances For
        source
        @[implicit_reducible]
        instance Aesop.Script.Tactic.instToMessageData :
        Lean.ToMessageData Tactic
        source
        def Aesop.Script.Tactic.unstructured (uTactic : UTactic) :
        Tactic
        Instances For
          source
          def Aesop.Script.Tactic.structured (uTactic : UTactic) (sTactic : STactic) :
          Tactic
          Instances For
            source
            @[reducible, inline]
            abbrev Aesop.Script.TacticBuilder :
            Type
            Instances For