mathlib documentation

tactic.local_cache

meta def tactic.local_cache.internal.save_data {α : Type} [reflected Type α] [has_reflect α] (dn : name) (a : α) [reflected α a] :
meta def tactic.local_cache.internal.load_data {α : Type} [reflected Type α] [has_reflect α] (dn : name) :
meta def tactic.local_cache.internal.run_once_under_name {α : Type} [reflected Type α] [has_reflect α] (t : tactic α) (cache_name : name) :
meta structure tactic.local_cache.internal.cache_scope  :
Type

This scope propogates the cache within a begin ... end or by block and its decendants.

This scope propogates the cache within an entire def/lemma.

Asks whether the namespace ns currently has a value-in-cache.

Gets the (optionally present) value-in-cache for ns.

Using the namespace ns as its key, when called for the first time run_once ns t runs t, then saves and returns the result. Upon subsequent invocations in the same tactic block, with the scope of the caching being inherited by child tactic blocks) we return the cached result directly.

You can configure the cached scope to be entire def/lemmas changing the optional cache_scope argument to cache_scope.def_local. Note: the caches backing each scope are different.

If α is just unit, this means we just run t once each tactic block.