mathlib3 documentation

tactic.local_cache

source
meta def tactic.local_cache.internal.mk_full_namespace (ns : name) :
name
source
meta def tactic.local_cache.internal.save_data {α : Type} [reflected Type α] [has_reflect α] (dn : name) (a : α) [reflected α a] :
tactic unit
source
meta def tactic.local_cache.internal.load_data {α : Type} [reflected Type α] [has_reflect α] (dn : name) :
tactic α
source
meta def tactic.local_cache.internal.poke_data (dn : name) :
tactic bool
source
meta def tactic.local_cache.internal.run_once_under_name {α : Type} [reflected Type α] [has_reflect α] (t : tactic α) (cache_name : name) :
tactic α
source
meta structure tactic.local_cache.internal.cache_scope  :
Type
source
meta def tactic.local_cache.internal.block_local.get_name (ns : name) :
tactic name
source
meta def tactic.local_cache.internal.block_local.try_get_name (ns : name) :
tactic name
source
meta def tactic.local_cache.internal.block_local.present (ns : name) :
tactic bool
source
meta def tactic.local_cache.internal.block_local.clear (ns : name) :
tactic unit
source
def tactic.local_cache.internal.def_local.FNV_OFFSET_BASIS  :
ℕ
Equations
source
def tactic.local_cache.internal.def_local.FNV_PRIME  :
ℕ
Equations
source
def tactic.local_cache.internal.def_local.RADIX  :
ℕ
Equations
source
def tactic.local_cache.internal.def_local.hash_byte (seed : ℕ) (c : char) :
ℕ
Equations
source
def tactic.local_cache.internal.def_local.hash_string (s : string) :
ℕ
Equations
source
meta def tactic.local_cache.internal.def_local.hash_context  :
tactic string
source
meta def tactic.local_cache.internal.def_local.get_root_name (ns : name) :
tactic name
source
meta def tactic.local_cache.internal.def_local.apply_tag (n : name) (tag : ℕ) :
name
source
meta def tactic.local_cache.internal.def_local.mk_dead_name (n : name) :
name
source
meta def tactic.local_cache.internal.def_local.kill_name (n : name) :
tactic unit
source
meta def tactic.local_cache.internal.def_local.is_name_dead (n : name) :
tactic bool
source
meta def tactic.local_cache.internal.def_local.get_tag_with_status (rn : name) :
tactic (ℕ × bool)
source
meta def tactic.local_cache.internal.def_local.get_name (ns : name) :
tactic name
source
meta def tactic.local_cache.internal.def_local.try_get_name (ns : name) :
tactic name
source
meta def tactic.local_cache.internal.def_local.present (ns : name) :
tactic bool
source
meta def tactic.local_cache.internal.def_local.clear (ns : name) :
tactic unit
source
meta def tactic.local_cache.cache_scope.block_local  :
tactic.local_cache.internal.cache_scope

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

source
meta def tactic.local_cache.cache_scope.def_local  :
tactic.local_cache.internal.cache_scope

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

source
meta def tactic.local_cache.present (ns : name) (s : tactic.local_cache.internal.cache_scope := tactic.local_cache.cache_scope.block_local) :
tactic bool

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

source
meta def tactic.local_cache.clear (ns : name) (s : tactic.local_cache.internal.cache_scope := tactic.local_cache.cache_scope.block_local) :
tactic unit

Clear cache associated to namespace ns.

source
meta def tactic.local_cache.get (ns : name) (α : Type) [reflected Type α] [has_reflect α] (s : tactic.local_cache.internal.cache_scope := tactic.local_cache.cache_scope.block_local) :
tactic (option α)

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

source
meta def tactic.run_once {α : Type} [reflected Type α] [has_reflect α] (ns : name) (t : tactic α) (s : tactic.local_cache.internal.cache_scope := tactic.local_cache.cache_scope.block_local) :
tactic α

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.