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.

source
@[inline]
abbrev Lean.KeyedDeclsAttribute.Key:
Type
Equations
source
structure Lean.KeyedDeclsAttribute.Def (γ : Type) :
Type

KeyedDeclsAttribute definition.

Important: mkConst valueTypeName and γ must be definitionally equal.

source
instance Lean.KeyedDeclsAttribute.instInhabitedDef:
{a : Type} → Inhabited (Lean.KeyedDeclsAttribute.Def a)
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.KeyedDeclsAttribute.OLeanEntry:
Type
source
instance Lean.KeyedDeclsAttribute.instInhabitedOLeanEntry:
Inhabited Lean.KeyedDeclsAttribute.OLeanEntry
Equations
source
structure Lean.KeyedDeclsAttribute.AttributeEntry (γ : Type) extends Lean.KeyedDeclsAttribute.OLeanEntry :
Type
  • value : γ
source
@[inline]
abbrev Lean.KeyedDeclsAttribute.Table (γ : Type) :
Type
Equations
source
structure Lean.KeyedDeclsAttribute.ExtensionState (γ : Type) :
Type
source
instance Lean.KeyedDeclsAttribute.instInhabitedExtensionState:
{a : Type} → Inhabited (Lean.KeyedDeclsAttribute.ExtensionState a)
Equations
  • Lean.KeyedDeclsAttribute.instInhabitedExtensionState = { default := { newEntries := default, table := default, declNames := default, erased := default } }
source
@[inline]
abbrev Lean.KeyedDeclsAttribute.Extension (γ : Type) :
Type
Equations
source
structure Lean.KeyedDeclsAttribute (γ : Type) :
Type
source
instance Lean.instNonemptyKeyedDeclsAttribute {γ : Type} :
Nonempty (Lean.KeyedDeclsAttribute γ)
Equations
source
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.
source
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.
source
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.
source
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.
source
unsafe def Lean.KeyedDeclsAttribute.init {γ : Type} (df : Lean.KeyedDeclsAttribute.Def γ) (attrDeclName : Lean.Name) :
IO (Lean.KeyedDeclsAttribute γ)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
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