Documentation

Lean.LabelAttribute

"Label" attributes #

Allow creating attributes using register_label_attr, and retrieving the array of Names of declarations which have been tagged with such an attribute.

These differ slightly from the built-in "tag attributes" which can be initialized with the syntax:

initialize someName : TagAttribute ← registerTagAttribute `tagName "description"

in that a "tag attribute" can only be put on a declaration at the moment it is declared, and can not be modified by scoping commands.

The "label attributes" constructed here support adding (or locally removing) the attribute either at the moment of declaration, or later.

@[reducible, inline]

An environment extension that just tracks an array of names.

Equations
    Instances For
      @[reducible, inline]

      The collection of all current LabelExtensions, indexed by name.

      Equations
        Instances For
          def Lean.mkLabelExt (name : Name := by exact decl_name%) :

          Helper function for registerLabelAttr.

          Equations
            Instances For
              def Lean.mkLabelAttr (attrName : Name) (attrDescr : String) (ext : LabelExtension) (ref : Name := by exact decl_name%) :

              Helper function for registerLabelAttr.

              Equations
                Instances For
                  def Lean.registerLabelAttr (attrName : Name) (attrDescr : String) (ref : Name := by exact decl_name%) :

                  Construct a new "label attribute", which does nothing except keep track of the names of the declarations with that attribute.

                  Users will generally use the register_label_attr macro defined below.

                  Equations
                    Instances For

                      Initialize a new "label" attribute. Declarations tagged with the attribute can be retrieved using Lean.labelled.

                      Equations
                        Instances For
                          def Lean.labelled (attrName : Name) :

                          When attrName is an attribute created using register_labelled_attr, return the names of all declarations labelled using that attribute.

                          Equations
                            Instances For