From 4b2da5700a809a288aadae50c753a0b1ee738d43 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 30 Jan 2025 22:22:22 +0100 Subject: [PATCH] style --- Cache/IO.lean | 4 ++-- Cache/Lean.lean | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Cache/IO.lean b/Cache/IO.lean index 0da48ab0b073d..f57896652f5fb 100644 --- a/Cache/IO.lean +++ b/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 diff --git a/Cache/Lean.lean b/Cache/Lean.lean index 768e408f2b4b1..a3ded1a61baeb 100644 --- a/Cache/Lean.lean +++ b/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