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.

source
@[reducible, inline]
abbrev Lean.KeyedDeclsAttribute.Key :
Type
Equations

- Lean.KeyedDeclsAttribute.Key = Lean.Name

Instances For

source
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

Instances For

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

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

source
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 }

Instances For

source
structure Lean.KeyedDeclsAttribute.OLeanEntry :
Type

- key : Key
- declName : Name

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

Instances For

source
instance Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry :
Inhabited OLeanEntry
Equations

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

source
def Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry.default :
OLeanEntry
Equations

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

Instances For

source
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`.

Instances For

source
@[reducible, inline]
abbrev Lean.KeyedDeclsAttribute.Table (γ : Type) :
Type
Equations

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

Instances For

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

- newEntries : List OLeanEntry
- table : Table γ
- declNames : PHashSet Name
- erased : PHashSet Name

Instances For

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

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

Instances For

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

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

source
@[reducible, inline]
abbrev Lean.KeyedDeclsAttribute.Extension (γ : Type) :
Type
Equations

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

Instances For

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

- defn : Def γ
- tableRef : IO.Ref (Table γ)
- ext : Extension γ

Instances For

source
instance Lean.instNonemptyKeyedDeclsAttribute {γ✝ : Type} :
Nonempty (KeyedDeclsAttribute γ✝)
source
def Lean.KeyedDeclsAttribute.ExtensionState.insert {γ : Type} (s : ExtensionState γ) (v : AttributeEntry γ) :
ExtensionState γ
Equations

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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)

Instances For