Documentation

Std.Time.Zoned.Database.Windows

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
    def Std.Time.Database.Windows.getZoneRules.toLocalTime (res : TimeZone) :
    TimeZone.LocalTimeType
    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
          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.