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.

• )

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 Std.Time.TimeZone.instReprOffset : Repr Offset

instance Std.Time.TimeZone.instDecidableEqOffset : DecidableEq Offset

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

instance Std.Time.TimeZone.instInhabitedOffset : Inhabited Offset

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.