mathlib3 documentation

core / init.meta.attribute

source
meta constant attribute.get_instances  :
name → tactic (list name)

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 (cache_ty : 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.
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 (cache_ty param_ty : 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.
source
meta def attribute.register (decl : 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} (attr : user_attribute α β) :
tactic α

Returns the attribute cache for the given user attribute.

source
meta def user_attribute.parse_reflect {α β : Type} (attr : user_attribute α β) :
lean.parser expr
source
meta constant user_attribute.get_param_untyped {α β : Type} (attr : user_attribute α β) (decl : name) :
tactic expr
source
meta constant user_attribute.set_untyped {α β : Type} [reflected Type β] (attr : user_attribute α β) (decl : name) (val : expr) (persistent : bool) (prio : option ℕ := option.none) :
tactic unit
source
meta def user_attribute.get_param {α β : Type} [reflected Type β] (attr : user_attribute α β) (n : name) :
tactic β

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

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

Alias for attribute.register

source
meta def get_attribute_cache_dyn {α : Type} [reflected Type α] (attr_decl_name : name) :
tactic α
source
meta def mk_name_set_attr (attr_name : name) :
tactic unit
source
meta def get_name_set_for_attr (name : _root_.name) :
tactic name_set