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

@[instance_reducible]

instance Std.Time.TimeZone.instReprOffset : Repr Offset

@[instance_reducible]

instance Std.Time.TimeZone.instDecidableEqOffset : DecidableEq Offset

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

@[instance_reducible]

instance Std.Time.TimeZone.instInhabitedOffset : Inhabited Offset

@[instance_reducible]

instance Std.Time.TimeZone.instOrdOffset : Ord Offset

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").

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

A zero Offset representing UTC (no offset).

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

Creates an Offset from a given number of hour.

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

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

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_reducible]

instance Std.Time.instInhabitedTimeZone : Inhabited TimeZone

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

@[instance_reducible]

instance Std.Time.instReprTimeZone : Repr TimeZone

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

@[instance_reducible]

instance Std.Time.instDecidableEqTimeZone : DecidableEq TimeZone

def Std.Time.TimeZone.UTC : TimeZone

A zeroed Timezone representing UTC (no offset).

def Std.Time.TimeZone.GMT : TimeZone

A zeroed Timezone representing GMT (no offset).

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

Creates a Timestamp from a given number of hour.

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

Creates a Timestamp from a given number of second.

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

Gets the number of seconds in a timezone offset.

@[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.

@[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.

@[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.

@[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.