Def Cache.IO.cleanCache

Modification history

2025-07-23 01:41
Cache/IO.lean
chore: update Cache for compatibility with nightly (#27376) …
Modified Cache.IO.cleanCacheView on Github →
2025-02-11 17:01
Cache/IO.lean
chore(Cache): stylistic change to not use `default` (#21707) …
Modified Cache.IO.cleanCacheView on Github →
2023-01-04 18:18
Cache/IO.lean
fix: multiple cache bugs (#1333) …
Added Cache.IO.cleanCacheView on Github →