Idris2Doc : IotaTime.Tzdb.Windows.Types

IotaTime.Tzdb.Windows.Types

(source)
Definitions
record WindowsTransitionDate : Type
  Recurring SYSTEMTIME fields used by Windows TZI registry values.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindowsTransitionDate : Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> WindowsTransitionDate

  Projections:
  
.hour : WindowsTransitionDate -> Integer
  
.minute : WindowsTransitionDate -> Integer
  
.month : WindowsTransitionDate -> Integer
  
.second : WindowsTransitionDate -> Integer
  
.week : WindowsTransitionDate -> Integer
  
.weekday : WindowsTransitionDate -> Integer
  
.year : WindowsTransitionDate -> Integer
.year : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
year : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.month : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
month : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.week : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
week : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.weekday : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
weekday : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.hour : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
hour : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.minute : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
minute : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
.second : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
second : WindowsTransitionDate -> Integer
  Totality: total
  Visibility: public export
record WindowsZoneRule : Type
  The recurring portion of a Windows REG_TZI_FORMAT value. Bias fields are
  minutes added to local time to obtain UTC, following Windows conventions.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindowsZoneRule : Integer -> Integer -> Integer -> String -> String -> WindowsTransitionDate -> WindowsTransitionDate -> WindowsZoneRule

  Projections:
  
.biasMinutes : WindowsZoneRule -> Integer
  
.daylightBiasMinutes : WindowsZoneRule -> Integer
  
.daylightName : WindowsZoneRule -> String
  
.daylightStart : WindowsZoneRule -> WindowsTransitionDate
  
.standardBiasMinutes : WindowsZoneRule -> Integer
  
.standardName : WindowsZoneRule -> String
  
.standardStart : WindowsZoneRule -> WindowsTransitionDate
.biasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
biasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
.standardBiasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
standardBiasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
.daylightBiasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
daylightBiasMinutes : WindowsZoneRule -> Integer
  Totality: total
  Visibility: public export
.standardName : WindowsZoneRule -> String
  Totality: total
  Visibility: public export
standardName : WindowsZoneRule -> String
  Totality: total
  Visibility: public export
.daylightName : WindowsZoneRule -> String
  Totality: total
  Visibility: public export
daylightName : WindowsZoneRule -> String
  Totality: total
  Visibility: public export
.daylightStart : WindowsZoneRule -> WindowsTransitionDate
  Totality: total
  Visibility: public export
daylightStart : WindowsZoneRule -> WindowsTransitionDate
  Totality: total
  Visibility: public export
.standardStart : WindowsZoneRule -> WindowsTransitionDate
  Totality: total
  Visibility: public export
standardStart : WindowsZoneRule -> WindowsTransitionDate
  Totality: total
  Visibility: public export
record WindowsDynamicRule : Type
  A Dynamic DST registry value effective from January 1 of its year.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindowsDynamicRule : Integer -> WindowsZoneRule -> WindowsDynamicRule

  Projections:
  
.dynamicRule : WindowsDynamicRule -> WindowsZoneRule
  
.effectiveYear : WindowsDynamicRule -> Integer
.effectiveYear : WindowsDynamicRule -> Integer
  Totality: total
  Visibility: public export
effectiveYear : WindowsDynamicRule -> Integer
  Totality: total
  Visibility: public export
.dynamicRule : WindowsDynamicRule -> WindowsZoneRule
  Totality: total
  Visibility: public export
dynamicRule : WindowsDynamicRule -> WindowsZoneRule
  Totality: total
  Visibility: public export
record WindowsRegistryZone : Type
  Platform-neutral data read from one Windows time-zone registry key.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindowsRegistryZone : String -> String -> String -> List Bits8 -> List (Integer, List Bits8) -> WindowsRegistryZone

  Projections:
  
.registryDaylightName : WindowsRegistryZone -> String
  
.registryDefaultTzi : WindowsRegistryZone -> List Bits8
  
.registryDynamicTzi : WindowsRegistryZone -> List (Integer, List Bits8)
  
.registryStandardName : WindowsRegistryZone -> String
  
.registryZoneId : WindowsRegistryZone -> String
.registryZoneId : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
registryZoneId : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
.registryStandardName : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
registryStandardName : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
.registryDaylightName : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
registryDaylightName : WindowsRegistryZone -> String
  Totality: total
  Visibility: public export
.registryDefaultTzi : WindowsRegistryZone -> List Bits8
  Totality: total
  Visibility: public export
registryDefaultTzi : WindowsRegistryZone -> List Bits8
  Totality: total
  Visibility: public export
.registryDynamicTzi : WindowsRegistryZone -> List (Integer, List Bits8)
  Totality: total
  Visibility: public export
registryDynamicTzi : WindowsRegistryZone -> List (Integer, List Bits8)
  Totality: total
  Visibility: public export
record WindowsRegistrySnapshot : Type
  Complete result emitted by a native Windows registry source.

  Totality: total
  Visibility: public export
  Constructor: 
MkWindowsRegistrySnapshot : String -> List WindowsRegistryZone -> WindowsRegistrySnapshot

  Projections:
  
.snapshotLocalZoneId : WindowsRegistrySnapshot -> String
  
.snapshotZones : WindowsRegistrySnapshot -> List WindowsRegistryZone
.snapshotLocalZoneId : WindowsRegistrySnapshot -> String
  Totality: total
  Visibility: public export
snapshotLocalZoneId : WindowsRegistrySnapshot -> String
  Totality: total
  Visibility: public export
.snapshotZones : WindowsRegistrySnapshot -> List WindowsRegistryZone
  Totality: total
  Visibility: public export
snapshotZones : WindowsRegistrySnapshot -> List WindowsRegistryZone
  Totality: total
  Visibility: public export
data WindowsZoneError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
WindowsOffsetOutOfRange : Integer -> WindowsZoneError
  
WindowsTimeOutOfRange : Integer -> Integer -> Integer -> WindowsZoneError
  
WindowsTransitionMillisecondsUnsupported : Integer -> WindowsZoneError
  
WindowsAbsoluteTransitionUnsupported : Integer -> WindowsZoneError
  
IncompleteWindowsDaylightRule : WindowsZoneError
  
WindowsTziLength : Integer -> WindowsZoneError
  
WindowsRecurrenceError : RecurrenceRuleError -> WindowsZoneError
data WindowsTimeZoneError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
InvalidWindowsRule : WindowsZoneError -> WindowsTimeZoneError
  
InvalidWindowsTransitions : TimeZoneError -> WindowsTimeZoneError
  
DynamicYearsNotStrictlyIncreasing : WindowsTimeZoneError
data WindowsRegistryError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
InvalidDefaultTzi : WindowsZoneError -> WindowsRegistryError
  
InvalidDynamicTzi : Integer -> WindowsZoneError -> WindowsRegistryError
  
InvalidRegistryTimeZone : WindowsTimeZoneError -> WindowsRegistryError
data WindowsRegistryProtocolError : Type
  Totality: total
  Visibility: public export
  Constructors:
  
MissingLocalZoneId : WindowsRegistryProtocolError
  
UnexpectedRegistryLine : String -> WindowsRegistryProtocolError
  
InvalidRegistryHex : String -> WindowsRegistryProtocolError
  
InvalidDynamicRegistryLine : String -> WindowsRegistryProtocolError
  
IncompleteRegistryZone : WindowsRegistryProtocolError