structure Std.Time.TimeZone.Offset : Type

Represents a timezone offset with an hour and second component.

• ofSeconds :: (
• second : Second.Offset

  The same timezone offset in seconds.

• )

Instances For

• Std.Time.TimeZone.instInhabitedOffset
• Std.Time.TimeZone.instLawfulEqOrdOffset
• Std.Time.TimeZone.instOrdOffset
• Std.Time.TimeZone.instReprOffset
• Std.Time.TimeZone.instTransOrdOffset

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

instance Std.Time.TimeZone.instReprOffset : Repr Offset

Equations

• Std.Time.TimeZone.instReprOffset = { reprPrec := Std.Time.TimeZone.reprOffset✝ }

instance Std.Time.TimeZone.instDecidableEqOffset : DecidableEq Offset

Equations

• Std.Time.TimeZone.instDecidableEqOffset = Std.Time.TimeZone.decEqOffset✝

instance Std.Time.TimeZone.instInhabitedOffset : Inhabited Offset

Equations

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

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 }