source
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

source
theorem Std.Time.TimeZone.Offset.ext_iff {x y : Offset} :
x = y ↔ x.second = y.second
source
theorem Std.Time.TimeZone.Offset.ext {x y : Offset} (second : x.second = y.second) :
x = y
source
def Std.Time.TimeZone.instReprOffset.repr :
Offset → Nat → Std.Format
Equations

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

Instances For

source
instance Std.Time.TimeZone.instReprOffset :
Repr Offset
Equations

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

source
instance Std.Time.TimeZone.instDecidableEqOffset :
DecidableEq Offset
Equations

- Std.Time.TimeZone.instDecidableEqOffset = Std.Time.TimeZone.instDecidableEqOffset.decEq

source
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 ⋯

Instances For

source
instance Std.Time.TimeZone.instInhabitedOffset :
Inhabited Offset
Equations

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

source
instance Std.Time.TimeZone.instOrdOffset :
Ord Offset
Equations

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

source
theorem Std.Time.TimeZone.Offset.compare_def :
compare = compareOn fun (x : Offset) => x.second
source
instance Std.Time.TimeZone.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.TimeZone.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
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.

Instances For

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

A zero `Offset` representing UTC (no offset).

Equations

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

Instances For

source
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 }

Instances For

source
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 }

Instances For