Skip to content

Commit

Permalink
chore: shake Std.Time (#6283)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
hargoniX authored Dec 2, 2024
1 parent be63c82 commit 95dbac2
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 1 deletion.
1 change: 1 addition & 0 deletions src/Std/Time/DateTime/Timestamp.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 0 additions & 1 deletion src/Std/Time/Internal/UnitVal.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/Std/Time/Zoned/Database/Windows.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 95dbac2

Please sign in to comment.