Equations
- tactic.local_cache.internal.def_local.FNV_OFFSET_BASIS = 14695981039346656037
Equations
- tactic.local_cache.internal.def_local.FNV_PRIME = 1099511628211
Equations
- tactic.local_cache.internal.def_local.RADIX = 18446744073709551616
Equations
- tactic.local_cache.internal.def_local.hash_byte seed c = let n : ℕ := c.to_nat in seed.lxor n * tactic.local_cache.internal.def_local.FNV_PRIME % tactic.local_cache.internal.def_local.RADIX
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.
Clear cache associated to namespace ns.
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.