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.instBEqOffset
• Std.Time.TimeZone.instInhabitedOffset
• Std.Time.TimeZone.instReprOffset

instance Std.Time.TimeZone.instReprOffset : Repr Offset

Equations

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

instance Std.Time.TimeZone.instInhabitedOffset : Inhabited Offset

Equations

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

instance Std.Time.TimeZone.instBEqOffset : BEq 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 : 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 }