mathlib documentation

core / init.meta.attribute

meta constant attribute.get_instances  :

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.

meta constant attribute.fingerprint  :

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

meta structure user_attribute_cache_cfg (cache_ty : Type) :

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.

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

meta structure user_attribute (cache_ty param_ty : Type := unit) :

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


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.
meta def attribute.register (decl : name) :

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.

meta constant user_attribute.get_cache {α β : Type} (attr : user_attribute α β) :

Returns the attribute cache for the given user attribute.

meta def user_attribute.parse_reflect {α β : Type} (attr : user_attribute α β) :

meta constant user_attribute.get_param_untyped {α β : Type} (attr : user_attribute α β) (decl : name) :

meta constant user_attribute.set_untyped {α β : Type} [reflected β] (attr : user_attribute α β) (decl : name) (val : expr) (persistent : bool) (prio : option := none) :

meta def user_attribute.get_param {α β : Type} [reflected β] (attr : user_attribute α β) (n : name) :

Get the value of the parameter for the attribute on a given declatation. Will fail if the attribute does not exist.

meta def user_attribute.set {α β : Type} [reflected β] (attr : user_attribute α β) (n : name) (val : β) (persistent : bool) (prio : option := none) :

meta def register_attribute (decl : name) :

Alias for attribute.register

meta def get_attribute_cache_dyn {α : Type} [reflected α] (attr_decl_name : name) :

meta def mk_name_set_attr (attr_name : name) :