structure Std.Time.TimeZone.Offset : Type

Represents a timezone offset with an hour and second component.

• ofSeconds :: (
• second : Std.Time.Second.Offset

  The same timezone offset in seconds.

• )

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

Equations

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

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

Equations

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

instance Std.Time.TimeZone.instBEqOffset : BEq Std.Time.TimeZone.Offset

Equations

• Std.Time.TimeZone.instBEqOffset = { beq := fun (x y : Std.Time.TimeZone.Offset) => x.second == y.second }

def Std.Time.TimeZone.Offset.toIsoString (offset : Std.Time.TimeZone.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 : Std.Time.TimeZone.Offset

A zero Offset representing UTC (no offset).

Equations

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

def Std.Time.TimeZone.Offset.ofHours (n : Std.Time.Hour.Offset) : Std.Time.TimeZone.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 : Std.Time.Hour.Offset) (m : Std.Time.Minute.Offset) : Std.Time.TimeZone.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 }