Documentation

Aesop.Script.Tactic

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