mathlib docs: core.init.meta.attribute

Get all of the declaration names that have the given attribute. Eg. get_instances `simp returns a list with the names of all of the lemmas in the environment tagged with the @[simp] attribute.

source

meta constant attribute.fingerprint :

name → tactic ℕ

Returns a hash of get_instances. You can use this to tell if your attribute instances have changed.

source

meta structure user_attribute_cache_cfg :

Type → Type

mk_cache : list name → tactic cache_ty
dependencies : list name

Configuration for a user attribute cache. For example, the simp attribute has a cache of type simp_lemmas.

mk_cache is a function where you are given all of the declarations tagged with your attribute and you return the new value for the cache. That is, mk_cache makes the object you want to be cached.
dependencies is a list of other attributes whose caches need to be computed first.

source

meta def user_attribute.dflt_cache_cfg :

tactic unit

Close the current goal by filling it with the trivial user_attribute_cache_cfg unit.

source

meta def user_attribute.dflt_parser :

tactic unit

source

meta structure user_attribute :

(Type := unit) → (Type := unit) → Type

name : name
descr : string
after_set : option (name → ℕ → bool → tactic unit)
before_unset : option (name → bool → tactic unit)
cache_cfg : user_attribute_cache_cfg cache_ty . "dflt_cache_cfg"
reflect_param : has_reflect param_ty
parser : lean.parser param_ty . "dflt_parser"

A __user attribute__ is an attribute defined by the user (ie, not built in to Lean).

Type parameters

cache_ty is the type of a cached VM object that is computed from all of the declarations in the environment tagged with this attribute.
param_ty is an argument for the attribute when it is used. For instance with param_ty being ℕ you could write @[my_attribute 4].

Data

A user_attribute consists of the following pieces of data:

name is the name of the attribute, eg simp
descr is a plaintext description of the attribute for humans.
after_set is an optional handler that will be called after the attribute has been applied to a declaration. Failing the tactic will fail the entire attribute/def/... command, i.e. the attribute will not be applied after all. Declaring an after_set handler without a before_unset handler will make the attribute non-removable.
before_unset Optional handler that will be called before the attribute is removed from a declaration.
cache_cfg describes how to construct the user attribute's cache. See docstring for user_attribute_cache_cfg
reflect_param demands that param_ty can be reflected. This means we have a function from param_ty to an expr. See the docstring for has_reflect.
parser Parser that will be invoked after parsing the attribute's name. The parse result will be reflected and stored and can be retrieved with user_attribute.get_param.

source

meta def attribute.register :

name → tactic unit

Registers a new user-defined attribute. The argument must be the name of a definition of type user_attribute α β. Once registered, you may tag declarations with this attribute.

source

meta constant user_attribute.get_cache {α β : Type} :

user_attribute α β → tactic α

Returns the attribute cache for the given user attribute.

source

meta def user_attribute.parse_reflect {α β : Type} :

user_attribute α β → lean.parser expr

source

meta constant user_attribute.get_param_untyped {α β : Type} :

user_attribute α β → name → tactic expr

source

meta constant user_attribute.set_untyped {α β : Type} [reflected β] :