source
structure Lean.TagAttributeExtra :
Type

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

- ext : PersistentEnvExtension Name Name NameSet

  The environment extension for the attribute.

- base : NameHashSet

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

Instances For

source
instance Lean.instInhabitedTagAttributeExtra :
Inhabited TagAttributeExtra
Equations

- Lean.instInhabitedTagAttributeExtra = { default := Lean.instInhabitedTagAttributeExtra.default }

source
def Lean.instInhabitedTagAttributeExtra.default :
TagAttributeExtra
Equations

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

Instances For

source
def Lean.registerTagAttributeExtra (name : Name) (descr : String) (extra : List Name) (validate : Name → AttrM Unit := fun (x : Name) => pure ()) (ref : Name := by exact decl_name%) :
IO 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.

Instances For

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

Does declaration `decl` have the tag `attr`?

Equations

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

Instances For

source
def Lean.TagAttributeExtra.getDecls (attr : TagAttributeExtra) (env : Environment) :
Array 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.

Instances For

source
structure Lean.ParametricAttributeExtra (α : Type) :
Type

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

- attr : ParametricAttribute α

  The underlying `ParametricAttribute`.

- base : Std.HashMap Name α

  A list of pre-tagged declarations with their values.

Instances For

source
instance Lean.instInhabitedParametricAttributeExtra {a✝ : Type} :
Inhabited (ParametricAttributeExtra a✝)
Equations

- Lean.instInhabitedParametricAttributeExtra = { default := Lean.instInhabitedParametricAttributeExtra.default }

source
def Lean.instInhabitedParametricAttributeExtra.default {a✝ : Type} :
ParametricAttributeExtra a✝
Equations

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

Instances For

source
def Lean.registerParametricAttributeExtra {α : Type} (impl : ParametricAttributeImpl α) (extra : List (Name × α)) :
IO (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.

Instances For

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

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

Equations

- attr.getParam? env decl = (attr.attr.getParam? env decl <|> attr.base[decl]?)

Instances For

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

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

Equations

- attr.setParam env decl param = attr.attr.setParam env decl param

Instances For