# Documentation

Mathlib.Tactic.Cache

# Once-per-file cache for tactics #

This file defines cache data structures for tactics that are initialized the first time they are accessed. Since Lean 4 starts one process per file, these caches are once-per-file and can for example be used to cache information about the imported modules.

The Cache α data structure is the most generic version we define. It is created using Cache.mk f where f : MetaM α performs the initialization of the cache:

initialize numberOfImports : Cache Nat ← Cache.mk do
(← getEnv).imports.size

-- (does not work in the same module where the cache is defined)
#eval show MetaM Nat from numberOfImports.get


The DeclCache α data structure computes a fold over the environment's constants: DeclCache.mk empty f constructs such a cache where empty : α and f : Name → ConstantInfo → α → MetaM α. The result of the constants in the imports is cached between tactic invocations, while for constants defined in the same file f is evaluated again every time. This kind of cache can be used e.g. to populate discrimination trees.

Once-per-file cache.

Equations
def Mathlib.Tactic.Cache.mk {α : Type} (init : ) :

Creates a cache with an initialization function.

Equations
def Mathlib.Tactic.Cache.get {m : } {α : Type} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (cache : ) :
m α

Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.

Equations
• One or more equations did not get rendered due to their size.

Cached fold over the environment's declarations, where a given function is applied to α for every constant.

Equations
def Mathlib.Tactic.DeclCache.mk {α : Type} (profilingName : String) (empty : α) (addDecl : Lean.NameLean.ConstantInfoα) :

Creates a DeclCache. The cached structure α is initialized with empty, and then addDecl is called for every constant in the environment. Calls to addDecl for imported constants are cached.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.DeclCache.get {α : Type} (cache : ) :

Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.

Equations
• One or more equations did not get rendered due to their size.