Documentation

Aesop.Rule

Normalisation Rules #

Instances For
    Equations
    @[inline, reducible]
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.

      Safe and Almost Safe Rules #

      inductive Aesop.Safety :
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Equations
          @[inline, reducible]
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.

            Unsafe Rules #

            Instances For
              Equations
              Equations
              @[inline, reducible]
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.

                Regular Rules #

                Equations
                • One or more equations did not get rendered due to their size.
                @[inline]
                def Aesop.RegularRule.withRule {β : Sort u_1} (f : {α : Type} → Aesop.Rule αβ) :
                Equations
                Instances For

                  Normalisation Simp Rules #

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Instances For
                        Equations
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For