Commit 2025-02-11 14:10 00823c9e

View on Github →

chore(Cache): rename HashMap to ModuleHashMap (#21704) Rename Cache.IO.HashMap to Cache.IO.ModuleHashMap to avoid confusion with Std.HashMap and deprecated Lean.HashMap

Estimated changes

modified def Cache.IO.lookup
modified def Cache.IO.packCache
modified def Cache.IO.unpackCache
modified def Cache.Requests.commit