Documentation

Aesop.Rule

Normalisation Rules #

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

                Safe and Almost Safe Rules #

                inductive Aesop.Safety :
                Instances For
                  Instances For
                    @[reducible, inline]
                    Equations
                      Instances For
                        Equations
                          Instances For

                            Unsafe Rules #

                            Instances For
                              @[reducible, inline]
                              Equations
                                Instances For

                                  Regular Rules #

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

                                                          A local rule for the norm simplifier.

                                                          Instances For
                                                            Instances For
                                                              Equations
                                                                Instances For