Documentation

Lean.KeyedDeclsAttribute

A builder for attributes that are applied to declarations of a common type and group them by the given attribute argument (an arbitrary Name, currently). Also creates a second "builtin" attribute used for bootstrapping, which saves the applied declarations in an IO.Ref instead of an environment extension.

Used to register elaborators, macros, tactics, and delaborators.

@[reducible, inline]
Equations
Instances For

    KeyedDeclsAttribute definition.

    Important: mkConst valueTypeName and γ must be definitionally equal.

    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Instances For
          Equations
          • Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := { newEntries := default, table := default, declNames := default, erased := 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
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Retrieve entries tagged with [attr key] or [builtinAttr key].

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

                    Retrieve values tagged with [attr key] or [builtinAttr key].

                    Equations
                    • attr.getValues env key = List.map Lean.KeyedDeclsAttribute.AttributeEntry.value (attr.getEntries env key)
                    Instances For