structure Std.Time.TimeZone.Offset : Type

Represents a timezone offset as a total number of seconds from UTC.

• ofSeconds :: (
• second : Second.Offset

  The same timezone offset in seconds.

• )

theorem Std.Time.TimeZone.Offset.ext_iff {x y : Offset} : x = y ↔ x.second = y.second

theorem Std.Time.TimeZone.Offset.ext {x y : Offset} (second : x.second = y.second) : x = y

def Std.Time.TimeZone.instReprOffset.repr : Offset → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Std.Time.TimeZone.instReprOffset : Repr Offset

Equations

• Std.Time.TimeZone.instReprOffset = { reprPrec := Std.Time.TimeZone.instReprOffset.repr }

@[implicit_reducible]

instance Std.Time.TimeZone.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.TimeZone.instDecidableEqOffset = Std.Time.TimeZone.instDecidableEqOffset.decEq

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

Equations

• Std.Time.TimeZone.instDecidableEqOffset.decEq { second := a } { second := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Std.Time.TimeZone.instInhabitedOffset : Inhabited Offset

Equations

• Std.Time.TimeZone.instInhabitedOffset = { default := { second := 0 } }

@[implicit_reducible]

instance Std.Time.TimeZone.instOrdOffset : Ord Offset

Equations

• Std.Time.TimeZone.instOrdOffset = { compare := compareOn fun (x : Std.Time.TimeZone.Offset) => x.second }

theorem Std.Time.TimeZone.Offset.compare_def : compare = compareOn fun (x : Offset) => x.second

instance Std.Time.TimeZone.instTransOrdOffset : TransOrd Offset

instance Std.Time.TimeZone.instLawfulEqOrdOffset : LawfulEqOrd Offset

def Std.Time.TimeZone.Offset.toIsoString (offset : Offset) (colon : Bool) : String

Converts an Offset to a string in ISO 8601 format. The colon parameter determines if the hour and minute components are separated by a colon (e.g., "+01:00" or "+0100").

Equations

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

def Std.Time.TimeZone.Offset.zero : Offset

A zero Offset representing UTC (no offset).

Equations

• Std.Time.TimeZone.Offset.zero = { second := 0 }

def Std.Time.TimeZone.Offset.ofHours (n : Hour.Offset) : Offset

Creates an Offset from a given number of hour.

Equations

• Std.Time.TimeZone.Offset.ofHours n = { second := n.toSeconds }

def Std.Time.TimeZone.Offset.ofHoursAndMinutes (n : Hour.Offset) (m : Minute.Offset) : Offset

Creates an Offset from a given number of hours and minutes.

Equations

• Std.Time.TimeZone.Offset.ofHoursAndMinutes n m = { second := n.toSeconds + m.toSeconds }

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.

@[implicit_reducible]

instance Std.Time.instInhabitedTimeZone : Inhabited TimeZone

Equations

• Std.Time.instInhabitedTimeZone = { default := Std.Time.instInhabitedTimeZone.default }

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

Equations

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

@[implicit_reducible]

instance Std.Time.instReprTimeZone : Repr TimeZone

Equations

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

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

Equations

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

@[implicit_reducible]

instance Std.Time.instDecidableEqTimeZone : DecidableEq TimeZone

Equations

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

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

@[inline]

def Std.Time.Timestamp.toWallTime (ts : Timestamp) (offset : TimeZone.Offset) : WallTime

Converts a Timestamp to a WallTime for a given timezone offset. The result is the local civil time: wall = UTC + offset.

Equations

• ts.toWallTime offset = Std.Time.WallTime.ofDuration (ts.val + Std.Time.Duration.ofSeconds offset.second)

@[inline]

def Std.Time.Timestamp.ofWallTime (wt : WallTime) (offset : TimeZone.Offset) : Timestamp

Creates a Timestamp from a WallTime and a timezone offset. Assumes the WallTime represents civil time at the given offset: UTC = wall − offset.

Equations

• Std.Time.Timestamp.ofWallTime wt offset = Std.Time.Timestamp.ofDurationSinceUnixEpoch (wt.val - Std.Time.Duration.ofSeconds offset.second)

@[inline]

def Std.Time.WallTime.toTimestamp (wt : WallTime) (offset : TimeZone.Offset) : Timestamp

Converts a WallTime to a Timestamp given a timezone offset. The WallTime is treated as civil time at the given offset: UTC = wall − offset.

Equations

• wt.toTimestamp offset = Std.Time.Timestamp.ofWallTime wt offset

@[inline]

def Std.Time.WallTime.ofTimestamp (ts : Timestamp) (offset : TimeZone.Offset) : WallTime

Creates a WallTime from a Timestamp given a timezone offset. The result is the local civil time: wall = UTC + offset.

Equations

• Std.Time.WallTime.ofTimestamp ts offset = ts.toWallTime offset