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.

@[inline, reducible]
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
                  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
                      Instances For