structure Time.ZonedTime : Type

• localTime : Time.LocalTime
• timeZone : Time.TimeZone

instance Time.instReprZonedTime : Repr Time.ZonedTime

Equations

• Time.instReprZonedTime = { reprPrec := Time.reprZonedTime✝ }

instance Time.instBEqZonedTime : BEq Time.ZonedTime

Equations

• Time.instBEqZonedTime = { beq := Time.beqZonedTime✝ }

instance Time.instToStringZonedTime : ToString Time.ZonedTime

Equations

• Time.instToStringZonedTime = { toString := fun (a : Time.ZonedTime) => toString "" ++ toString a.localTime ++ toString ", " ++ toString a.timeZone ++ toString "" }

def Time.ZonedTime.getZonedTime : IO Time.ZonedTime

Equations

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

def Time.ZonedTime.sub (lt1 : Time.ZonedTime) (lt2 : Time.ZonedTime) : Time.DiffTime

Equations

• lt1.sub lt2 = Time.LocalTime.localTimeToUTCTime lt1.timeZone lt1.localTime - Time.LocalTime.localTimeToUTCTime lt2.timeZone lt2.localTime

instance Time.ZonedTime.instHSubDiffTime : HSub Time.ZonedTime Time.ZonedTime Time.DiffTime

Equations

• Time.ZonedTime.instHSubDiffTime = { hSub := Time.ZonedTime.sub }

instance Time.ZonedTime.instInhabited : Inhabited Time.ZonedTime

Equations

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