structure Std.Time.TimeZone : Type

A TimeZone structure that stores the timezone offset, the name, abbreviation and if it's in daylight saving time.

• offset : Offset

  The Offset of the date time.

• name : String

  The name of the time zone.

• abbreviation : String

  The abbreviation of the time zone.

• isDST : Bool

  Day light saving flag.

instance Std.Time.instInhabitedTimeZone : Inhabited TimeZone

Equations

• Std.Time.instInhabitedTimeZone = { default := { offset := default, name := default, abbreviation := default, isDST := default } }

instance Std.Time.instReprTimeZone : Repr TimeZone

Equations

• Std.Time.instReprTimeZone = { reprPrec := Std.Time.reprTimeZone✝ }

instance Std.Time.instDecidableEqTimeZone : DecidableEq TimeZone

Equations

• Std.Time.instDecidableEqTimeZone = Std.Time.decEqTimeZone✝

def Std.Time.TimeZone.UTC : TimeZone

A zeroed Timezone representing UTC (no offset).

Equations

• Std.Time.TimeZone.UTC = { offset := Std.Time.TimeZone.Offset.zero, name := "UTC", abbreviation := "UTC", isDST := false }

def Std.Time.TimeZone.GMT : TimeZone

A zeroed Timezone representing GMT (no offset).

Equations

• Std.Time.TimeZone.GMT = { offset := Std.Time.TimeZone.Offset.zero, name := "Greenwich Mean Time", abbreviation := "GMT", isDST := false }

def Std.Time.TimeZone.ofHours (name abbreviation : String) (n : Hour.Offset) (isDST : Bool := false) : TimeZone

Creates a Timestamp from a given number of hour.

Equations

• Std.Time.TimeZone.ofHours name abbreviation n isDST = { offset := Std.Time.TimeZone.Offset.ofHours n, name := name, abbreviation := abbreviation, isDST := isDST }

def Std.Time.TimeZone.ofSeconds (name abbreviation : String) (n : Second.Offset) (isDST : Bool := false) : TimeZone

Creates a Timestamp from a given number of second.

Equations

• Std.Time.TimeZone.ofSeconds name abbreviation n isDST = { offset := { second := n }, name := name, abbreviation := abbreviation, isDST := isDST }

def Std.Time.TimeZone.toSeconds (tz : TimeZone) : Second.Offset

Gets the number of seconds in a timezone offset.

Equations

• tz.toSeconds = tz.offset.second