source
@[extern lean_windows_get_next_transition]
opaque Std.Time.Database.Windows.getNextTransition :
String → Int64 → Bool → IO (Option (Int64 × TimeZone))

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

source
@[extern lean_get_windows_local_timezone_id_at]
opaque Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt :
Int64 → IO String

Fetches the timezone at a timestamp.

source
def Std.Time.Database.Windows.getZoneRules (id : String) :
IO 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.

Instances For

source
structure Std.Time.Database.WindowsDb :
Type

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

Instances For

source
@[inline]
def Std.Time.Database.WindowsDb.default :
WindowsDb

Returns a default `WindowsDb` instance.

Equations

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

Instances For

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

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