Documentation

Aesop.RuleTac.Tactic

Equations
    Instances For
      @[implemented_by Aesop.RuleTac.tacticMImpl]
      Equations
        Instances For
          @[implemented_by Aesop.RuleTac.ruleTacImpl]
          Equations
            Instances For
              @[implemented_by Aesop.RuleTac.singleRuleTacImpl]

              Elaborates and runs the given tactic syntax stx. The syntax stx must be of kind tactic or tacticSeq.

              Equations
                Instances For
                  Equations
                    Instances For
                      @[implemented_by Aesop.RuleTac.tacGenImpl]