Documentation

Lean.Attributes

@[inline]
abbrev Lean.AttrM (α : Type) :
Type
Equations
Equations
structure Lean.AttributeImplCore :
Type
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
def Lean.registerTagAttribute (name : Lean.Name) (descr : String) (validate : optParam (Lean.NameLean.AttrM Unit) fun x => pure ()) :
Equations
Equations
  • Lean.instInhabitedParametricAttribute = { default := { attr := default, ext := default } }
structure Lean.ParametricAttributeImpl (α : Type) extends Lean.AttributeImplCore :
Type
Equations
def Lean.ParametricAttribute.getParam {α : Type} [inst : Inhabited α] (attr : Lean.ParametricAttribute α) (env : Lean.Environment) (decl : Lean.Name) :
Equations
Equations
Equations
  • Lean.instInhabitedEnumAttributes = { default := { attrs := default, ext := default } }
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) :
Equations
def Lean.EnumAttributes.getValue {α : Type} [inst : Inhabited α] (attr : Lean.EnumAttributes α) (env : Lean.Environment) (decl : Lean.Name) :
Equations
Equations
Equations
Equations
Equations
Equations
@[implementedBy Lean.mkAttributeImplOfConstantUnsafe]
Equations
Equations
Equations
Equations
Equations
def Lean.Attribute.erase (declName : Lean.Name) (attrName : Lean.Name) :
Equations