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 := Std.Time.instInhabitedTimeZone.default }

def Std.Time.instInhabitedTimeZone.default : TimeZone

Equations

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

def Std.Time.instReprTimeZone.repr : TimeZone → Nat → Std.Format

Equations

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

instance Std.Time.instReprTimeZone : Repr TimeZone

Equations

• Std.Time.instReprTimeZone = { reprPrec := Std.Time.instReprTimeZone.repr }

instance Std.Time.instDecidableEqTimeZone : DecidableEq TimeZone

Equations

• Std.Time.instDecidableEqTimeZone = Std.Time.instDecidableEqTimeZone.decEq

def Std.Time.instDecidableEqTimeZone.decEq (x✝ x✝¹ : TimeZone) : Decidable (x✝ = x✝¹)

Equations

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

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