diff --git a/src/Std/Time/Zoned/ZoneRules.lean b/src/Std/Time/Zoned/ZoneRules.lean index 72253c6d05f2..e196a3f84dbb 100644 --- a/src/Std/Time/Zoned/ZoneRules.lean +++ b/src/Std/Time/Zoned/ZoneRules.lean @@ -148,7 +148,7 @@ If the timestamp falls between two transitions, it returns the most recent trans def findTransitionIndexForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Nat := let value := timestamp.toSecondsSinceUnixEpoch if let some idx := transitions.findIdx? (fun t => t.time.val ≥ value.val) - then some (idx - 1) + then some idx else none /--