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]

abbrev Lean.KeyedDeclsAttribute.Key : Type

Equations

• Lean.KeyedDeclsAttribute.Key = Lean.Name

def Lean.KeyedDeclsAttribute.evalIdentKey (stx : Syntax) : AttrM Key

Equations

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

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

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) (key : Key) : AttrM Unit

def Lean.KeyedDeclsAttribute.instInhabitedDef.default {a✝ : Type} : Def a✝

Equations

• Lean.KeyedDeclsAttribute.instInhabitedDef.default = { builtinName := default, name := default, descr := default, valueTypeName := default, evalKey := default, onAdded := default }

@[implicit_reducible]

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

Equations

• Lean.KeyedDeclsAttribute.instInhabitedDef = { default := Lean.KeyedDeclsAttribute.instInhabitedDef.default }

structure Lean.KeyedDeclsAttribute.OLeanEntry : Type

• key : Key
• declName : Name

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

@[implicit_reducible]

instance Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry : Inhabited OLeanEntry

Equations

• Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry = { default := Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry.default }

def Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry.default : OLeanEntry

Equations

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

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

• key : Key
• declName : Name
• isBuiltin : Bool
• 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.

@[reducible, 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 OLeanEntry
• table : Table γ
• declNames : PHashSet Name
• erased : PHashSet Name

@[implicit_reducible]

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

Equations

• Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := Lean.KeyedDeclsAttribute.instInhabitedExtensionState.default }

def Lean.KeyedDeclsAttribute.instInhabitedExtensionState.default {a✝ : Type} : ExtensionState a✝

Equations

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

@[reducible, 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 : Def γ
• tableRef : IO.Ref (Table γ)
• ext : Extension γ

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Def γ) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ)

Equations

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

def Lean.KeyedDeclsAttribute.getEntries {γ : Type} (attr : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List (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 : KeyedDeclsAttribute γ) (env : Environment) (key : Name) : List γ

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

Equations

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