Def Cache.Hashing.HashMemo.filterByFilePaths

Modification history

2025-04-03 01:55
Cache/Hashing.lean
refactor(Cache): use module name as key instead of unresolved file path (#21834) …
Deleted Cache.Hashing.HashMemo.filterByFilePathsView on Github →
2025-02-11 14:10
Cache/Hashing.lean
chore(Cache): rename HashMap to ModuleHashMap (#21704) …
Modified Cache.Hashing.HashMemo.filterByFilePathsView on Github →
2023-01-10 18:51
Cache/Hashing.lean
feat: specific file names for `cache get` and `cache get!` (#1430) …
Added Cache.Hashing.HashMemo.filterByFilePathsView on Github →