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