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]

abbrev Lean.KeyedDeclsAttribute.Key : Type

Equations

• Lean.KeyedDeclsAttribute.Key = Lean.Name

structure Lean.KeyedDeclsAttribute.Def (γ : Type) : Type

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

  builtinName : Lean.Name

• Attribute name (e.g., `term_elab)

  name : Lean.Name

• Attribute description

  descr : String
• valueTypeName : Lean.Name

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

  evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key
• onAdded : Bool → Lean.Name → Lean.AttrM Unit

KeyedDeclsAttribute definition.

Important: mkConst valueTypeName and γ must be definitionally equal.

instance Lean.KeyedDeclsAttribute.instInhabitedDef : {a : Type} → Inhabited (Lean.KeyedDeclsAttribute.Def a)

Equations

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

structure Lean.KeyedDeclsAttribute.OLeanEntry : Type

• key : Lean.KeyedDeclsAttribute.Key

• Name of a declaration stored in the environment which has type mkConst Def.valueTypeName.

  declName : Lean.Name

instance Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry : Inhabited Lean.KeyedDeclsAttribute.OLeanEntry

Equations

• Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry = { default := { key := default, declName := default } }

structure Lean.KeyedDeclsAttribute.AttributeEntry (γ : Type) extends Lean.KeyedDeclsAttribute.OLeanEntry : Type

• 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.

  value : γ

@[inline]

abbrev Lean.KeyedDeclsAttribute.Table (γ : Type) : Type

Equations

• Lean.KeyedDeclsAttribute.Table γ = Lean.SMap Lean.KeyedDeclsAttribute.Key (List (Lean.KeyedDeclsAttribute.AttributeEntry γ))

structure Lean.KeyedDeclsAttribute.ExtensionState (γ : Type) : Type

• newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry
• table : Lean.KeyedDeclsAttribute.Table γ
• declNames : Lean.PHashSet Lean.Name
• erased : Lean.PHashSet Lean.Name

instance Lean.KeyedDeclsAttribute.instInhabitedExtensionState : {a : Type} → Inhabited (Lean.KeyedDeclsAttribute.ExtensionState a)

Equations

• Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := { newEntries := default, table := default, declNames := default, erased := default } }

@[inline]

abbrev Lean.KeyedDeclsAttribute.Extension (γ : Type) : Type

Equations

• Lean.KeyedDeclsAttribute.Extension γ = Lean.ScopedEnvExtension Lean.KeyedDeclsAttribute.OLeanEntry (Lean.KeyedDeclsAttribute.AttributeEntry γ) (Lean.KeyedDeclsAttribute.ExtensionState γ)

structure Lean.KeyedDeclsAttribute (γ : Type) : Type

• defn : Lean.KeyedDeclsAttribute.Def γ
• tableRef : IO.Ref (Lean.KeyedDeclsAttribute.Table γ)
• ext : Lean.KeyedDeclsAttribute.Extension γ

instance Lean.instNonemptyKeyedDeclsAttribute : ∀ {γ : Type}, Nonempty (Lean.KeyedDeclsAttribute γ)

Equations

• @Lean.instNonemptyKeyedDeclsAttribute = @Lean.instNonemptyKeyedDeclsAttribute.proof_1

def Lean.KeyedDeclsAttribute.ExtensionState.insert {γ : Type} (s : Lean.KeyedDeclsAttribute.ExtensionState γ) (v : Lean.KeyedDeclsAttribute.AttributeEntry γ) : Lean.KeyedDeclsAttribute.ExtensionState γ

Equations

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

def Lean.KeyedDeclsAttribute.addBuiltin {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (key : Lean.KeyedDeclsAttribute.Key) (declName : Lean.Name) (value : γ) : IO Unit

Equations

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

def Lean.KeyedDeclsAttribute.mkStateOfTable {γ : Type} (table : Lean.KeyedDeclsAttribute.Table γ) : Lean.KeyedDeclsAttribute.ExtensionState γ

Equations

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

def Lean.KeyedDeclsAttribute.ExtensionState.erase {γ : Type} (s : Lean.KeyedDeclsAttribute.ExtensionState γ) (attrName : Lean.Name) (declName : Lean.Name) : Lean.CoreM (Lean.KeyedDeclsAttribute.ExtensionState γ)

Equations

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

unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Lean.KeyedDeclsAttribute.Def γ) (attrDeclName : autoParam Lean.Name _auto✝) : IO (Lean.KeyedDeclsAttribute γ)

Equations

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

def Lean.KeyedDeclsAttribute.getEntries {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (env : Lean.Environment) (key : Lean.Name) : List (Lean.KeyedDeclsAttribute.AttributeEntry γ)

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

Equations

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

def Lean.KeyedDeclsAttribute.getValues {γ : Type} (attr : Lean.KeyedDeclsAttribute γ) (env : Lean.Environment) (key : Lean.Name) : List γ

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

Equations

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