@[extern lean_windows_get_next_transition]

opaque Std.Time.Database.Windows.getNextTransition : String → Int64 → Bool → IO (Option (Int64 × Std.Time.TimeZone))

Fetches the next timezone transition for a given timezone identifier and timestamp.

@[extern lean_get_windows_local_timezone_id_at]

opaque Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt : Int64 → IO String

Fetches the timezone at a timestamp.

def Std.Time.Database.Windows.getZoneRules (id : String) : IO Std.Time.TimeZone.ZoneRules

Retrieves the timezone rules, including all transitions, for a given timezone identifier.

Equations

• One or more equations did not get rendered due to their size.

def Std.Time.Database.Windows.getZoneRules.toLocalTime (res : Std.Time.TimeZone) : Std.Time.TimeZone.LocalTimeType

Equations

• One or more equations did not get rendered due to their size.

structure Std.Time.Database.WindowsDb : Type

Represents a Time Zone Database that we get from ICU available on Windows SDK.

@[inline]

def Std.Time.Database.WindowsDb.default : Std.Time.Database.WindowsDb

Returns a default WindowsDb instance.

Equations

• Std.Time.Database.WindowsDb.default = { }

instance Std.Time.Database.WindowsDb.inst : Std.Time.Database Std.Time.Database.WindowsDb

Equations

• One or more equations did not get rendered due to their size.