Documentation

Aesop.Rule

Normalisation Rules #

Instances For
    Equations
    @[reducible, inline]
    Equations
    Instances For
      Equations

      Safe and Almost Safe Rules #

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

            Unsafe Rules #

            Instances For
              Equations
              Equations
              @[reducible, inline]
              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.
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      @[inline]
                      def Aesop.RegularRule.withRule {β : Sort u_1} (f : {α : Type} → Aesop.Rule αβ) :
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For

                              Normalisation Simp Rules #

                              A global rule for the norm simplifier. Each SimpEntry represents a member of the simp set, e.g. a declaration whose type is an equality or a smart unfolding theorem for a declaration.

                              Instances For
                                Equations

                                A local rule for the norm simplifier.

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