"Label" attributes

Allow creating attributes using register_label_attr, and retrieving the array of Names of declarations which have been tagged with such an attribute.

These differ slightly from the built-in "tag attributes" which can be initialized with the syntax:

initialize someName : TagAttribute ← registerTagAttribute `tagName "description"

in that a "tag attribute" can only be put on a declaration at the moment it is declared, and can not be modified by scoping commands.

The "label attributes" constructed here support adding (or locally removing) the attribute either at the moment of declaration, or later.

@[inline, reducible]

abbrev Std.Tactic.LabelAttr.LabelExtension : Type

An environment extension that just tracks an array of names.

Equations

• Std.Tactic.LabelAttr.LabelExtension = Lean.SimpleScopedEnvExtension Lean.Name (Array Lean.Name)

@[inline, reducible]

abbrev Std.Tactic.LabelAttr.LabelExtensionMap : Type

The collection of all current LabelExtensions, indexed by name.

Equations

• Std.Tactic.LabelAttr.LabelExtensionMap = Lean.HashMap Lean.Name Std.Tactic.LabelAttr.LabelExtension

opaque Std.Tactic.LabelAttr.labelExtensionMapRef : IO.Ref Std.Tactic.LabelAttr.LabelExtensionMap

Store the current LabelExtensions.

def Std.Tactic.LabelAttr.mkLabelExt (name : autoParam Lean.Name _auto✝) : IO Std.Tactic.LabelAttr.LabelExtension

Helper function for registerLabelAttr.

Equations

• Std.Tactic.LabelAttr.mkLabelExt = Lean.registerSimpleScopedEnvExtension (Lean.SimpleScopedEnvExtension.Descr.mk (fun d e => if Array.contains d e = true then d else Array.push d e) #[] id)

def Std.Tactic.LabelAttr.mkLabelAttr (attrName : Lean.Name) (attrDescr : String) (ext : Std.Tactic.LabelAttr.LabelExtension) (ref : autoParam Lean.Name _auto✝) : IO Unit

Helper function for registerLabelAttr.

Equations

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

def Std.Tactic.LabelAttr.registerLabelAttr (attrName : Lean.Name) (attrDescr : String) (ref : autoParam Lean.Name _auto✝) : IO Std.Tactic.LabelAttr.LabelExtension

Construct a new "label attribute", which does nothing except keep track of the names of the declarations with that attribute.

Users will generally use the register_label_attr macro defined below.

Equations

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

def Lean.Parser.Command.registerLabelAttr : Lean.ParserDescr

Initialize a new "label" attribute. Declarations tagged with the attribute can be retrieved using Std.Tactic.LabelAttr.labelled.

Equations

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

def Std.Tactic.LabelAttr.labelled (attrName : Lean.Name) : Lean.CoreM (Array Lean.Name)

When attrName is an attribute created using register_labelled_attr, return the names of all declarations labelled using that attribute.

Equations

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