Cache

📁 Source: Batteries/Util/Cache.lean

Statistics

Metric	Count
Definitions Cache, get, mk, DeclCache, addDecl, addLibraryDecl, cache, get, mk, DiscrTreeCache, getMatch, mk, wrapAsync	13
Theorems instNonemptyCache, instNonemptyDeclCache	2
Total	15

Batteries.Tactic

Definitions

Name	Category	Theorems
Cache 📖	CompOp	1 math math: instNonemptyCache
DeclCache 📖	CompData	1 math math: instNonemptyDeclCache
DiscrTreeCache 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNonemptyCache 📖	mathematical	—	Cache	—	—
instNonemptyDeclCache 📖	mathematical	—	DeclCache	—	instNonemptyCache

Batteries.Tactic.Cache

Definitions

Name	Category	Theorems
get 📖	CompOp	—
mk 📖	CompOp	—

Batteries.Tactic.DeclCache

Definitions

Name	Category	Theorems
addDecl 📖	CompOp	—
addLibraryDecl 📖	CompOp	—
cache 📖	CompOp	—
get 📖	CompOp	—
mk 📖	CompOp	—

Batteries.Tactic.DiscrTreeCache

Definitions

Name	Category	Theorems
getMatch 📖	CompOp	—
mk 📖	CompOp	—

Lean.Meta

Definitions

Name	Category	Theorems
wrapAsync 📖	CompOp	—

---

← Back to Index