Documentation

Lean.Attributes

@[reducible, inline]
abbrev Lean.AttrM (α : Type) :
Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations

      You can tag attributes with the 'local' or 'scoped' kind. For example: attribute [local myattr, scoped yourattr, theirattr].

      This is used to indicate how an attribute should be scoped.

      • local means that the attribute should only be applied in the current scope and forgotten once the current section, namespace, or file is closed.
      • scoped means that the attribute should only be applied while the namespace is open.
      • global means that the attribute should always be applied.

      Note that the attribute handler (AttributeImpl.add) is responsible for interpreting the kind and making sure that these kinds are respected.

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

          Low level attribute registration function.

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

            Helper methods for decoding the parameters of builtin attributes that are defined before Lean.Parser. We have the following ones:

            @[builtin_attr_parser] def simple     := leading_parser ident >> optional (ppSpace >> (priorityParser <|> ident))
            @[builtin_attr_parser] def «macro»    := leading_parser "macro " >> ident
            @[builtin_attr_parser] def «export»   := leading_parser "export " >> ident
            

            Note that we need the parsers for class, instance, export and macros because they are keywords.

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

                        Tag attributes are simple and efficient. They are useful for marking declarations in the modules where they were defined.

                        The startup cost for this kind of attribute is very small since addImportedFn is a constant function.

                        They provide the predicate tagAttr.hasTag env decl which returns true iff declaration decl is tagged in the environment env.

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

                              A TagAttribute variant where we can attach parameters to attributes. It is slightly more expensive and consumes a little bit more memory than TagAttribute.

                              They provide the function pAttr.getParam env decl which returns some p iff declaration decl contains the attribute pAttr with parameter p.

                              Instances For
                                Equations
                                • Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        structure Lean.EnumAttributes (α : Type) :

                                        Given a list [a₁, ..., a_n] of elements of type α, EnumAttributes provides an attribute Attr_i for associating a value a_i with an declaration. α is usually an enumeration type. Note that whenever we register an EnumAttributes, we create n attributes, but only one environment extension.

                                        Instances For
                                          Equations
                                          • Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For

                                                Attribute extension and builders. We use builders to implement attribute factories for parser categories.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[implemented_by Lean.mkAttributeImplOfConstantUnsafe]
                                                    @[export lean_is_attribute]

                                                    Return true iff n is the name of a registered attribute.

                                                    Equations
                                                    Instances For

                                                      Return the name of all registered attributes.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[export lean_attribute_application_time]
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    Instances For
                                                                      def Lean.Attribute.erase (declName : Lake.Name) (attrName : Lake.Name) :
                                                                      Equations
                                                                      Instances For
                                                                        @[export lean_update_env_attributes]

                                                                        updateEnvAttributes implementation

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

                                                                          getNumBuiltinAttributes implementation

                                                                          Equations
                                                                          Instances For