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