Commit 2025-02-13 11:44 aed65172

View on Github →

chore(Cache): move helper functions to Cache.Lean (#21816) Move functions about basic Lean types to preliminary file in order to add more such helper functions in the future.

Estimated changes

Modified Cache/IO.lean

deleted def Nat.toHexDigits

deleted def System.FilePath.withoutParent

deleted def UInt64.asLTar

Created Cache/Lean.lean

added def Nat.toHexDigits

added def System.FilePath.withoutParent

added def UInt64.asLTar