style

Cache/IO.lean

@@ -262,10 +262,10 @@ If `keep` is true, the result will contain the entries that do exist;
 if `keep` is false, the result will contain the entries that do not exist.
 -/
 def filterExists (hashMap : HashMap) (keep : Bool) : IO HashMap :=
-  hashMap.foldM (init := default) fun acc path hash => do
+  hashMap.foldM (init := default) fun acc mod hash => do
     let exist ← (CACHEDIR / hash.asLTar).pathExists
     let add := if keep then exist else !exist
-    if add then return acc.insert path hash else return acc
+    if add then return acc.insert mod hash else return acc
 
 def hashes (hashMap : HashMap) : Lean.RBTree UInt64 compare :=
   hashMap.fold (init := default) fun acc _ hash => acc.insert hash

Cache/Lean.lean

@@ -66,7 +66,7 @@ will return `False` as the real system path is unknown to the function.
 
 For example, `contains (".." / "myFolder") ("myFolder" / "..")` will always return `false`
 even though it might be true depending on which local working directory on is in
-(which `contains` does'nt know about since it's not in `IO`.)
+(which `contains` doesn't know about since it's not in `IO`)
 -/
 def contains (path target : FilePath) : Bool :=
   go path.components target.components
@@ -77,7 +77,7 @@ where
     | path, "." :: target => go path target
     | "" :: path, target => go path target
     | path, "" :: target => go path target
-    -- must not start with ".."
+    -- must not start with unequal quantity of ".."
     | ".." :: path, ".." :: target => go path target
     | ".." :: _, _ => false
     | _, ".." :: _ => false