fix: problem with index in the timezone

leanprover · Nov 6, 2024 · d6e2024 · d6e2024
1 parent 35c014a
commit d6e2024
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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
 
 /--