From 95dbac26cff90f2a54806020ab4de77301a43892 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 2 Dec 2024 11:52:43 +0100
Subject: [PATCH] chore: shake Std.Time (#6283)

This PR reduces the import closure of `Std.Time` such that it doesn't
have to be rebuilt on every change in `Init.Data`.

Noticed while working on `Init` refactorings.
---
 src/Std/Time/DateTime/Timestamp.lean     | 1 +
 src/Std/Time/Internal/UnitVal.lean       | 1 -
 src/Std/Time/Zoned/Database/Windows.lean | 1 +
 3 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean
index f2c38ddea7b2..8ba43cc11892 100644
--- a/src/Std/Time/DateTime/Timestamp.lean
+++ b/src/Std/Time/DateTime/Timestamp.lean
@@ -6,6 +6,7 @@ Authors: Sofia Rodrigues
 prelude
 import Std.Time.Internal
 import Init.Data.Int
+import Init.System.IO
 import Std.Time.Time
 import Std.Time.Date
 import Std.Time.Duration
diff --git a/src/Std/Time/Internal/UnitVal.lean b/src/Std/Time/Internal/UnitVal.lean
index cc97c0b6481c..782b5c28d456 100644
--- a/src/Std/Time/Internal/UnitVal.lean
+++ b/src/Std/Time/Internal/UnitVal.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
-import Init.Data
 import Std.Internal.Rat
 
 namespace Std
diff --git a/src/Std/Time/Zoned/Database/Windows.lean b/src/Std/Time/Zoned/Database/Windows.lean
index 2a9a0bea23f3..80458d886eaf 100644
--- a/src/Std/Time/Zoned/Database/Windows.lean
+++ b/src/Std/Time/Zoned/Database/Windows.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
 prelude
+import Init.Data.SInt.Basic
 import Std.Time.DateTime
 import Std.Time.Zoned.TimeZone
 import Std.Time.Zoned.ZoneRules