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.

      • builtinName : Name

        Builtin attribute name, if any (e.g., `builtin_term_elab)

      • name : Name

        Attribute name (e.g., `term_elab)

      • descr : String

        Attribute description

      • valueTypeName : Name
      • evalKey (builtin : Bool) (stx : Syntax) : AttrM Key

        Convert Syntax into a Key, the default implementation expects an identifier.

      • onAdded (builtin : Bool) (declName : Name) : AttrM Unit
      Instances For
        Instances For
          • value : γ

            Recall that we cannot store γ into .olean files because it is a closure. Given OLeanEntry.declName, we convert it into a γ by using the unsafe function evalConstCheck.

          Instances For
            @[reducible, inline]
            Equations
              Instances For
                Instances For
                  @[reducible, inline]
                  Equations
                    Instances For
                      Instances For
                        def Lean.KeyedDeclsAttribute.addBuiltin {γ : Type} (attr : KeyedDeclsAttribute γ) (key : Key) (declName : Name) (value : γ) :
                        Equations
                          Instances For
                            Equations
                              Instances For
                                Equations
                                  Instances For
                                    unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Def γ) (attrDeclName : Name := by exact decl_name%) :
                                    Equations
                                      Instances For

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

                                        Equations
                                          Instances For

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

                                            Equations
                                              Instances For