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  :
Type → 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  :
(Type := unit)(Type := unit) → Type

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.
meta def attribute.register  :

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} :
user_attribute α βtactic α

Returns the attribute cache for the given user attribute.

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

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

meta constant user_attribute.set_untyped {α β : Type} [reflected β] :
user_attribute α βnameexprbool(option := none)tactic unit

meta def user_attribute.get_param {α β : Type} [reflected β] :
user_attribute α βnametactic β

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 β] :
user_attribute α βnameβ → bool(option := none)tactic unit

meta def register_attribute  :

Alias for attribute.register

meta def get_attribute_cache_dyn {α : Type} [reflected α] :
nametactic α