fix: problems with int64

leanprover · Nov 6, 2024 · a69dca1 · a69dca1
1 parent 1fc1f00
commit a69dca1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git 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
@@ -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,