max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unused imports (#6305)

Browse source 
This PR removes an unused import in the time library that can yield to
import cycles when building stuff that gets imported by `Std.Internal`
but also wants to import `Std.Time`.
This commit is contained in:
Henrik Böving 2024-12-04 13:46:08 +01:00 • committed by GitHub
parent c5181569f9
commit faf07e58db
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Std/Time/Zoned/DateTime.lean
View file

@ -6,7 +6,6 @@ Authors: Sofia Rodrigues
prelude
import Std.Time.DateTime
import Std.Time.Zoned.TimeZone
import Std.Internal
namespace Std
namespace Time