source
structure Std.Time.TimeZone.TZif.Header :
Type

Represents the header of a TZif file, containing metadata about the file's structure.

- version : UInt8

  The version of the TZif file format.

- isutcnt : UInt32

  The count of UT local indicators in the file.

- isstdcnt : UInt32

  The count of standard/wall indicators in the file.

- leapcnt : UInt32

  The number of leap second records.

- timecnt : UInt32

  The number of transition times in the file.

- typecnt : UInt32

  The number of local time types in the file.

- charcnt : UInt32

  The total number of characters used in abbreviations.

Instances For

source
instance Std.Time.TimeZone.TZif.instReprHeader :
Repr Header
Equations

- Std.Time.TimeZone.TZif.instReprHeader = { reprPrec := Std.Time.TimeZone.TZif.instReprHeader.repr }

source
def Std.Time.TimeZone.TZif.instReprHeader.repr :
Header → Nat → Std.Format
Equations

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

Instances For

source
instance Std.Time.TimeZone.TZif.instInhabitedHeader :
Inhabited Header
Equations

- Std.Time.TimeZone.TZif.instInhabitedHeader = { default := Std.Time.TimeZone.TZif.instInhabitedHeader.default }

source
def Std.Time.TimeZone.TZif.instInhabitedHeader.default :
Header
Equations

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

Instances For

source
structure Std.Time.TimeZone.TZif.LocalTimeType :
Type

Represents the local time type information, including offset and daylight saving details.

- gmtOffset : Int

  The GMT offset in seconds for this local time type.

- isDst : Bool

  Indicates if this local time type observes daylight saving time.

- abbreviationIndex : UInt8

  The index into the abbreviation string table for this time type.

Instances For

source
instance Std.Time.TimeZone.TZif.instReprLocalTimeType :
Repr LocalTimeType
Equations

- Std.Time.TimeZone.TZif.instReprLocalTimeType = { reprPrec := Std.Time.TimeZone.TZif.instReprLocalTimeType.repr }

source
def Std.Time.TimeZone.TZif.instReprLocalTimeType.repr :
LocalTimeType → Nat → Std.Format
Equations

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

Instances For

source
def Std.Time.TimeZone.TZif.instInhabitedLocalTimeType.default :
LocalTimeType
Equations

- Std.Time.TimeZone.TZif.instInhabitedLocalTimeType.default = { gmtOffset := default, isDst := default, abbreviationIndex := default }

Instances For

source
instance Std.Time.TimeZone.TZif.instInhabitedLocalTimeType :
Inhabited LocalTimeType
Equations

- Std.Time.TimeZone.TZif.instInhabitedLocalTimeType = { default := Std.Time.TimeZone.TZif.instInhabitedLocalTimeType.default }

source
structure Std.Time.TimeZone.TZif.LeapSecond :
Type

Represents a leap second record, including the transition time and the correction applied.

- transitionTime : Int

  The transition time of the leap second event.

- correction : Int

  The correction applied during the leap second event in seconds.

Instances For

source
instance Std.Time.TimeZone.TZif.instReprLeapSecond :
Repr LeapSecond
Equations

- Std.Time.TimeZone.TZif.instReprLeapSecond = { reprPrec := Std.Time.TimeZone.TZif.instReprLeapSecond.repr }

source
def Std.Time.TimeZone.TZif.instReprLeapSecond.repr :
LeapSecond → Nat → Std.Format
Equations

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

Instances For

source
instance Std.Time.TimeZone.TZif.instInhabitedLeapSecond :
Inhabited LeapSecond
Equations

- Std.Time.TimeZone.TZif.instInhabitedLeapSecond = { default := Std.Time.TimeZone.TZif.instInhabitedLeapSecond.default }

source
def Std.Time.TimeZone.TZif.instInhabitedLeapSecond.default :
LeapSecond
Equations

- Std.Time.TimeZone.TZif.instInhabitedLeapSecond.default = { transitionTime := default, correction := default }

Instances For

source
structure Std.Time.TimeZone.TZif.TZifV1 :
Type

Represents version 1 of the TZif format.

- header : Header

  The header information of the TZif file.

- transitionTimes : Array Int

  The array of transition times in seconds since the epoch.

- transitionIndices : Array UInt8

  The array of local time type indices corresponding to each transition time.

- localTimeTypes : Array LocalTimeType

  The array of local time type structures.

- abbreviations : Array String

  The array of abbreviation strings used by local time types.

- leapSeconds : Array LeapSecond

  The array of leap second records.

- stdWallIndicators : Array Bool

  The array indicating whether each transition time uses wall clock time or standard time.

- utLocalIndicators : Array Bool

  The array indicating whether each transition time uses universal time or local time.

Instances For

source
def Std.Time.TimeZone.TZif.instReprTZifV1.repr :
TZifV1 → Nat → Std.Format
Equations

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

Instances For

source
instance Std.Time.TimeZone.TZif.instReprTZifV1 :
Repr TZifV1
Equations

- Std.Time.TimeZone.TZif.instReprTZifV1 = { reprPrec := Std.Time.TimeZone.TZif.instReprTZifV1.repr }

source
instance Std.Time.TimeZone.TZif.instInhabitedTZifV1 :
Inhabited TZifV1
Equations

- Std.Time.TimeZone.TZif.instInhabitedTZifV1 = { default := Std.Time.TimeZone.TZif.instInhabitedTZifV1.default }

source
def Std.Time.TimeZone.TZif.instInhabitedTZifV1.default :
TZifV1
Equations

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

Instances For

source
structure Std.Time.TimeZone.TZif.TZifV2 extends Std.Time.TimeZone.TZif.TZifV1 :
Type

Represents version 2 of the TZif format, extending TZifV1 with an optional footer.

- header : Header
- transitionTimes : Array Int
- transitionIndices : Array UInt8
- localTimeTypes : Array LocalTimeType
- abbreviations : Array String
- leapSeconds : Array LeapSecond
- stdWallIndicators : Array Bool
- utLocalIndicators : Array Bool
- footer : Option String

  An optional footer for additional metadata in version 2.

Instances For

source
instance Std.Time.TimeZone.TZif.instReprTZifV2 :
Repr TZifV2
Equations

- Std.Time.TimeZone.TZif.instReprTZifV2 = { reprPrec := Std.Time.TimeZone.TZif.instReprTZifV2.repr }

source
def Std.Time.TimeZone.TZif.instReprTZifV2.repr :
TZifV2 → Nat → Std.Format
Equations

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

Instances For

source
instance Std.Time.TimeZone.TZif.instInhabitedTZifV2 :
Inhabited TZifV2
Equations

- Std.Time.TimeZone.TZif.instInhabitedTZifV2 = { default := Std.Time.TimeZone.TZif.instInhabitedTZifV2.default }

source
def Std.Time.TimeZone.TZif.instInhabitedTZifV2.default :
TZifV2
Equations

- Std.Time.TimeZone.TZif.instInhabitedTZifV2.default = { toTZifV1 := default, footer := default }

Instances For

source
structure Std.Time.TimeZone.TZif.TZif :
Type

Represents a TZif file, which can be either version 1 or version 2.

- v1 : TZifV1

  The data for version 1 of the TZif file.

- v2 : Option TZifV2

  Optionally, the data for version 2 of the TZif file.

Instances For

source
instance Std.Time.TimeZone.TZif.instReprTZif :
Repr TZif
Equations

- Std.Time.TimeZone.TZif.instReprTZif = { reprPrec := Std.Time.TimeZone.TZif.instReprTZif.repr }

source
def Std.Time.TimeZone.TZif.instReprTZif.repr :
TZif → Nat → Std.Format
Equations

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

Instances For

source
def Std.Time.TimeZone.TZif.instInhabitedTZif.default :
TZif
Equations

- Std.Time.TimeZone.TZif.instInhabitedTZif.default = { v1 := default, v2 := default }

Instances For

source
instance Std.Time.TimeZone.TZif.instInhabitedTZif :
Inhabited TZif
Equations

- Std.Time.TimeZone.TZif.instInhabitedTZif = { default := Std.Time.TimeZone.TZif.instInhabitedTZif.default }

source
def Std.Time.TimeZone.TZif.parse :
Internal.Parsec.ByteArray.Parser TZif

Parses a TZif file, which may be in either version 1 or version 2 format.

Equations

- Std.Time.TimeZone.TZif.parse = do let v1 ← Std.Time.TimeZone.TZif.parseTZifV1✝ let v2 ← Std.Time.TimeZone.TZif.parseTZifV2✝ pure { v1 := v1, v2 := v2 }

Instances For