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]

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
Equations
  • Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := { newEntries := default, table := default, declNames := default, erased := default } }
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Lean.KeyedDeclsAttribute.Def γ) (attrDeclName : Lean.Name := by exact decl_name%) :

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

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