Documentation

Mathlib.Tactic.Attr.Register

Attributes used in Mathlib #

In this file we define all simp-like and label-like attributes used in Mathlib. We declare all of them in one file for two reasons:

Simp set for functor_norm

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

    Simplification procedure

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

      Simp set for functor_norm

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

        Simplification procedure

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

          The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

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

            Simplification procedure

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

              Simp attribute for lemmas about Even

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

                Simplification procedure

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

                  "Simp attribute for lemmas about RCLike"

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

                    Simplification procedure

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

                      Simplification procedure

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

                        The simpset rify_simps is used by the tactic rify to move expressions from , , or to .

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

                          The simpset qify_simps is used by the tactic qify to move expressions from or to which gives a well-behaved division.

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

                            Simplification procedure

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

                              The simpset zify_simps is used by the tactic zify to move expressions from to which gives a well-behaved subtraction.

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

                                Simplification procedure

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

                                  The simpset mfld_simps records several simp lemmas that are especially useful in manifolds. It is a subset of the whole set of simp lemmas, but it makes it possible to have quicker proofs (when used with squeeze_simp or simp only) while retaining readability.

                                  The typical use case is the following, in a file on manifolds: If simp [foo, bar] is slow, replace it with squeeze_simp [foo, bar, mfld_simps] and paste its output. The list of lemmas should be reasonable (contrary to the output of squeeze_simp [foo, bar] which might contain tens of lemmas), and the outcome should be quick enough.

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

                                    Simplification procedure

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

                                      Simp set for integral rules.

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

                                        Simplification procedure

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

                                          Simplification procedure

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

                                            simp set for the manipulation of typevec and arrow expressions

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

                                              Simplification rules for ghost equations.

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

                                                Simplification procedure

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

                                                  Simplification procedure

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

                                                    The @[nontriviality] simp set is used by the nontriviality tactic to automatically discharge theorems about the trivial case (where we know Subsingleton α and many theorems in e.g. groups are trivially true).

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

                                                      A stub attribute for is_poly.

                                                      Equations
                                                      Instances For

                                                        Simplification procedure

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

                                                          A simp set for the fin_omega wrapper around omega.

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