Documentation

Lean.Attributes

source
inductive Lean.AttributeApplicationTime:
Type
source
instance Lean.instInhabitedAttributeApplicationTime:
Inhabited Lean.AttributeApplicationTime
Equations
source
instance Lean.instBEqAttributeApplicationTime:
BEq Lean.AttributeApplicationTime
Equations
source
@[inline]
abbrev Lean.AttrM (α : Type) :
Type
Equations
source
instance Lean.instMonadLiftImportMAttrM:
MonadLift Lean.ImportM Lean.AttrM
Equations
source
structure Lean.AttributeImplCore:
Type
source
instance Lean.instInhabitedAttributeImplCore:
Inhabited Lean.AttributeImplCore
Equations
source
inductive Lean.AttributeKind:
Type
source
instance Lean.instBEqAttributeKind:
BEq Lean.AttributeKind
Equations
source
instance Lean.instInhabitedAttributeKind:
Inhabited Lean.AttributeKind
Equations
source
instance Lean.instToStringAttributeKind:
ToString Lean.AttributeKind
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.AttributeImplextends Lean.AttributeImplCore :
Type
source
instance Lean.instInhabitedAttributeImpl:
Inhabited Lean.AttributeImpl
Equations
source
opaque Lean.attributeMapRef:
IO.Ref (Std.PersistentHashMap Lean.Name Lean.AttributeImpl)
source
def Lean.registerBuiltinAttribute (attr : Lean.AttributeImpl) :
IO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.Builtin.ensureNoArgs (stx : Lean.Syntax) :
Lean.AttrM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.Builtin.getIdent? (stx : Lean.Syntax) :
Lean.AttrM (Option Lean.Syntax)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.Builtin.getIdent (stx : Lean.Syntax) :
Lean.AttrM Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.Builtin.getId? (stx : Lean.Syntax) :
Lean.AttrM (Option Lean.Name)
Equations
source
def Lean.Attribute.Builtin.getId (stx : Lean.Syntax) :
Lean.AttrM Lean.Name
Equations
source
def Lean.getAttrParamOptPrio (optPrioStx : Lean.Syntax) :
Lean.AttrM Nat
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.Builtin.getPrio (stx : Lean.Syntax) :
Lean.AttrM Nat
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.TagAttribute:
Type

Tag attributes are simple and efficient. They are useful for marking declarations in the modules where they were defined.

The startup cost for this kind of attribute is very small since addImportedFn is a constant function.

They provide the predicate tagAttr.hasTag env decl which returns true iff declaration decl is tagged in the environment env.

source
instance Lean.instInhabitedTagAttribute:
Inhabited Lean.TagAttribute
Equations
source
def Lean.registerTagAttribute (name : Lean.Name) (descr : String) (validate : optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) :
IO Lean.TagAttribute
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.TagAttribute.hasTag (attr : Lean.TagAttribute) (env : Lean.Environment) (decl : Lean.Name) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.ParametricAttribute (α : Type) :
Type

A TagAttribute variant where we can attach parameters to attributes. It is slightly more expensive and consumes a little bit more memory than TagAttribute.

They provide the function pAttr.getParam env decl which returns some p iff declaration decl contains the attribute pAttr with parameter p.

source
instance Lean.instInhabitedParametricAttribute:
{a : Type} → Inhabited (Lean.ParametricAttribute a)
Equations
  • Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
source
structure Lean.ParametricAttributeImpl (α : Type) extends Lean.AttributeImplCore :
Type
source
def Lean.registerParametricAttribute {α : Type} [inst : Inhabited α] (impl : Lean.ParametricAttributeImpl α) :
IO (Lean.ParametricAttribute α)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.ParametricAttribute.getParam {α : Type} [inst : Inhabited α] (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.Name) :
Option α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.ParametricAttribute.setParam {α : Type} (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.Name) (param : α) :
Except String Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.EnumAttributes (α : Type) :
Type
source
instance Lean.instInhabitedEnumAttributes:
{a : Type} → Inhabited (Lean.EnumAttributes a)
Equations
  • Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
source
def Lean.registerEnumAttributes {α : Type} [inst : Inhabited α] (extName : Lean.Name) (attrDescrs : List (Lean.Name × String × α)) (validate : optParam (Lean.Name → α → Lean.AttrM Unit) fun x x => pure ()) (applicationTime : optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking) :
IO (Lean.EnumAttributes α)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.EnumAttributes.getValue {α : Type} [inst : Inhabited α] (attr : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.Name) :
Option α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.EnumAttributes.setValue {α : Type} (attrs : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.Name) (val : α) :
Except String Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
abbrev Lean.AttributeImplBuilder:
Type
Equations
source
@[inline]
abbrev Lean.AttributeImplBuilderTable:
Type
Equations
source
opaque Lean.attributeImplBuilderTableRef:
IO.Ref Lean.AttributeImplBuilderTable
source
def Lean.registerAttributeImplBuilder (builderId : Lean.Name) (builder : Lean.AttributeImplBuilder) :
IO Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.mkAttributeImplOfBuilder (builderId : Lean.Name) (args : List Lean.DataValue) :
IO Lean.AttributeImpl
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.AttributeExtensionOLeanEntry:
Type
source
structure Lean.AttributeExtensionState:
Type
source
instance Lean.instInhabitedAttributeExtensionState:
Inhabited Lean.AttributeExtensionState
Equations
source
@[inline]
abbrev Lean.AttributeExtension:
Type
Equations
source
unsafe def Lean.mkAttributeImplOfConstantUnsafe (env : Lean.Environment) (opts : Lean.Options) (declName : Lean.Name) :
Except String Lean.AttributeImpl
Equations
  • One or more equations did not get rendered due to their size.
source
@[implementedBy Lean.mkAttributeImplOfConstantUnsafe]
opaque Lean.mkAttributeImplOfConstant (env : Lean.Environment) (opts : Lean.Options) (declName : Lean.Name) :
Except String Lean.AttributeImpl
source
def Lean.mkAttributeImplOfEntry (env : Lean.Environment) (opts : Lean.Options) (e : Lean.AttributeExtensionOLeanEntry) :
IO Lean.AttributeImpl
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.attributeExtension:
Lean.AttributeExtension
source
@[export lean_is_attribute]
def Lean.isBuiltinAttribute (n : Lean.Name) :
IO Bool
Equations
source
def Lean.getBuiltinAttributeNames:
IO (List Lean.Name)
Equations
source
def Lean.getBuiltinAttributeImpl (attrName : Lean.Name) :
IO Lean.AttributeImpl
Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_attribute_application_time]
def Lean.getBuiltinAttributeApplicationTime (n : Lean.Name) :
IO Lean.AttributeApplicationTime
Equations
source
def Lean.isAttribute (env : Lean.Environment) (attrName : Lean.Name) :
Bool
Equations
source
def Lean.getAttributeNames (env : Lean.Environment) :
List Lean.Name
Equations
source
def Lean.getAttributeImpl (env : Lean.Environment) (attrName : Lean.Name) :
Except String Lean.AttributeImpl
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.registerAttributeOfDecl (env : Lean.Environment) (opts : Lean.Options) (attrDeclName : Lean.Name) :
Except String Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.registerAttributeOfBuilder (env : Lean.Environment) (builderId : Lean.Name) (args : List Lean.DataValue) :
IO Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Attribute.add (declName : Lean.Name) (attrName : Lean.Name) (stx : Lean.Syntax) (kind : optParam Lean.AttributeKind Lean.AttributeKind.global) :
Lean.AttrM Unit
Equations
source
def Lean.Attribute.erase (declName : Lean.Name) (attrName : Lean.Name) :
Lean.AttrM Unit
Equations
source
@[export lean_update_env_attributes]
def Lean.updateEnvAttributesImpl (env : Lean.Environment) :
IO Lean.Environment

updateEnvAttributes implementation

Equations
  • One or more equations did not get rendered due to their size.
source
@[export lean_get_num_attributes]
def Lean.getNumBuiltiAttributesImpl:
IO Nat

getNumBuiltinAttributes implementation

Equations