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.

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

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.

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

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.

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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.

@[implicit_reducible]

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

Equations

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

structure Std.Time.TimeZone.TZif.TZifV2extends 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.

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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.

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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 }