Configuration for a user attribute cache. For example, the
simp attribute has a cache of type simp_lemmas.
mk_cacheis 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_cachemakes the object you want to be cached.
dependenciesis a list of other attributes whose caches need to be computed first.
- 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).
cache_tyis the type of a cached VM object that is computed from all of the declarations in the environment tagged with this attribute.
param_tyis an argument for the attribute when it is used. For instance with
ℕyou could write
user_attribute consists of the following pieces of data:
nameis the name of the attribute, eg
descris a plaintext description of the attribute for humans.
after_setis 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_sethandler without a
before_unsethandler will make the attribute non-removable.
before_unsetOptional handler that will be called before the attribute is removed from a declaration.
cache_cfgdescribes how to construct the user attribute's cache. See docstring for
param_tycan be reflected. This means we have a function from
param_tyto an expr. See the docstring for
parserParser that will be invoked after parsing the attribute's name. The parse result will be reflected and stored and can be retrieved with