From a69dca171178ea2b03c9bef3f2c8f7828c8f243f Mon Sep 17 00:00:00 2001
From: Sofia Rodrigues <sofia@algebraic.dev>
Date: Wed, 6 Nov 2024 11:46:19 -0300
Subject: [PATCH] fix: problems with int64

---
 src/Std/Time/Duration.lean               | 3 +--
 src/Std/Time/Zoned/Database/Windows.lean | 6 +++---
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean
index 7549f0d4a13d..36a28d86f456 100644
--- a/src/Std/Time/Duration.lean
+++ b/src/Std/Time/Duration.lean
@@ -56,8 +56,7 @@ instance : Inhabited Duration where
 instance : OfNat Duration n where
   ofNat := by
     refine ⟨.ofInt n, ⟨0, by decide⟩, ?_⟩
-    simp <;> exact Int.le_total s.val 0 |>.symm
-    exact Int.le_total 0 n
+    simp <;> exact Int.le_total n 0 |>.symm
 
 namespace Duration
 
diff --git a/src/Std/Time/Zoned/Database/Windows.lean b/src/Std/Time/Zoned/Database/Windows.lean
index 241738c967bd..0ae44837832a 100644
--- a/src/Std/Time/Zoned/Database/Windows.lean
+++ b/src/Std/Time/Zoned/Database/Windows.lean
@@ -21,13 +21,13 @@ namespace Windows
 Fetches the next timezone transition for a given timezone identifier and timestamp.
 -/
 @[extern "lean_get_windows_next_transition"]
-opaque getNextTransition : @&String -> @&Int -> IO (Option (Int × TimeZone))
+opaque getNextTransition : @&String -> @&Int64 -> IO (Option (Int64 × TimeZone))
 
 /--
 Fetches the timezone at a timestamp.
 -/
 @[extern "lean_get_windows_local_timezone_id_at"]
-opaque getLocalTimeZoneIdentifierAt : @&Int → IO String
+opaque getLocalTimeZoneIdentifierAt : @&Int64 → IO String
 
 /--
 Retrieves the timezone rules, including all transitions, for a given timezone identifier.
@@ -39,7 +39,7 @@ def getZoneRules (id : String) : IO TimeZone.ZoneRules := do
   while true do
     let result ← Windows.getNextTransition id start
     if let some res := result then
-      transitions := transitions.push { time := Second.Offset.ofInt res.fst, localTimeType := {
+      transitions := transitions.push { time := Second.Offset.ofInt res.fst.toInt, localTimeType := {
         gmtOffset := res.snd.offset,
         abbreviation := res.snd.abbreviation,
         identifier := res.snd.name,