structure Time.UTCTime : Type

This is a representation of UTC. It consists of the day number, and a time offset from midnight.

• utctDay : Day
• utctDayTime : DiffTime

instance Time.instBEqUTCTime : BEq UTCTime

Equations

• Time.instBEqUTCTime = { beq := Time.instBEqUTCTime.beq }

def Time.instBEqUTCTime.beq : UTCTime → UTCTime → Bool

Equations

• Time.instBEqUTCTime.beq { utctDay := a, utctDayTime := a_1 } { utctDay := b, utctDayTime := b_1 } = (a == b && a_1 == b_1)
• Time.instBEqUTCTime.beq x✝¹ x✝ = false

instance Time.UTCTime.instToString : ToString UTCTime

Equations

• Time.UTCTime.instToString = { toString := fun (a : Time.UTCTime) => toString a.utctDay.modifiedJulianDay ++ toString ", " ++ toString a.utctDayTime }

def Time.UTCTime.systemEpochDay : Nat

unix epoch day as modified julian day

Equations

• Time.UTCTime.systemEpochDay = 40587

def Time.UTCTime.nominalDay : Nat

seconds of day

Equations

• Time.UTCTime.nominalDay = 86400

def Time.UTCTime.toUTCTime (now : { t : IO.FS.SystemTime // t.nsec.toNat < 10 ^ 9 }) : UTCTime

Equations

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

def Time.UTCTime.toDiffTime (utc : UTCTime) : DiffTime

Equations

• utc.toDiffTime = Time.DiffTime.fromSec (utc.utctDay.modifiedJulianDay * ↑Time.UTCTime.nominalDay) + utc.utctDayTime

def Time.UTCTime.sub (utc1 utc2 : UTCTime) : DiffTime

Equations

• utc1.sub utc2 = utc1.toDiffTime - utc2.toDiffTime

instance Time.UTCTime.instHSubDiffTime : HSub UTCTime UTCTime DiffTime

Equations

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