Documentation

Std.Time.Zoned.TimeZone

structure Std.Time.TimeZone :

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.

Instances For

instance Std.Time.instInhabitedTimeZone :

Inhabited TimeZone

Equations

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

instance Std.Time.instReprTimeZone :

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 :

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 :

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) :

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) :

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) :

Gets the number of seconds in a timezone offset.

Equations

tz.toSeconds = tz.offset.second