ink

structure Lean.TagAttributeExtra : Type

• The environment extension for the attribute.

  ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet

• A list of "base" declarations which have been pre-tagged.

  base : Lean.NameHashSet

TagAttributeExtra works around a limitation of TagAttribute, which is that definitions must be tagged in the same file that declares the definition. This works well for definitions in lean core, but for attributes declared outside the core this is problematic because we may want to tag declarations created before the attribute was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied in the same file as the declaration: During the declaration of the attribute itself, we can tag arbitrary other definitions, but once the attribute is declared we must tag things in the same file as normal.

ink

instance Lean.instInhabitedTagAttributeExtra : Inhabited Lean.TagAttributeExtra

Equations

• Lean.instInhabitedTagAttributeExtra = { default := { ext := default, base := default } }

ink

def Lean.registerTagAttributeExtra (name : Lean.Name) (descr : String) (extra : List Lean.Name) (validate : optParam (Lean.Name → Lean.AttrM Unit) fun x => pure ()) (ref : autoParam Lean.Name _auto✝) : IO Lean.TagAttributeExtra

Registers a new tag attribute. The extra field is a list of definitions from other modules which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same file as the declaration.

Note: The extra fields bypass the validate function - we assume the builtins are also pre-validated.

Equations

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

ink

def Lean.TagAttributeExtra.hasTag (attr : Lean.TagAttributeExtra) (env : Lean.Environment) (decl : Lean.Name) : Bool

Does declaration decl have the tag attr?

Equations

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

ink

def Lean.TagAttributeExtra.getDecls (attr : Lean.TagAttributeExtra) (env : Lean.Environment) : Array Lean.Name

Get the list of declarations tagged with the tag attribute attr.

Equations

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

ink

structure Lean.ParametricAttributeExtra (α : Type) : Type

• The underlying ParametricAttribute.

  attr : Lean.ParametricAttribute α

• A list of pre-tagged declarations with their values.

  base : Lean.HashMap Lean.Name α

ParametricAttributeExtra works around a limitation of ParametricAttribute, which is that definitions must be tagged in the same file that declares the definition. This works well for definitions in lean core, but for attributes declared outside the core this is problematic because we may want to tag declarations created before the attribute was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied in the same file as the declaration: During the declaration of the attribute itself, we can tag arbitrary other definitions, but once the attribute is declared we must tag things in the same file as normal.

ink

instance Lean.instInhabitedParametricAttributeExtra : {a : Type} → Inhabited (Lean.ParametricAttributeExtra a)

Equations

• Lean.instInhabitedParametricAttributeExtra = { default := { attr := default, base := default } }

ink

def Lean.registerParametricAttributeExtra {α : Type} [inst : Inhabited α] (impl : Lean.ParametricAttributeImpl α) (extra : List (Lean.Name × α)) : IO (Lean.ParametricAttributeExtra α)

Registers a new parametric attribute. The extra field is a list of definitions from other modules which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same file as the declaration.

Equations

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

ink

def Lean.ParametricAttributeExtra.getParam? {α : Type} [inst : Inhabited α] (attr : Lean.ParametricAttributeExtra α) (env : Lean.Environment) (decl : Lean.Name) : Option α

Gets the parameter of attribute attr associated to declaration decl, or none if decl is not tagged.

Equations

• Lean.ParametricAttributeExtra.getParam? attr env decl = HOrElse.hOrElse (Lean.ParametricAttribute.getParam? attr.attr env decl) fun x => Lean.HashMap.find? attr.base decl

ink

def Lean.ParametricAttributeExtra.setParam {α : Type} (attr : Lean.ParametricAttributeExtra α) (env : Lean.Environment) (decl : Lean.Name) (param : α) : Except String Lean.Environment

Applies attribute attr to declaration decl, given a value for the parameter.

Equations

• Lean.ParametricAttributeExtra.setParam attr env decl param = Lean.ParametricAttribute.setParam attr.attr env decl param