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.instReprUTCTime : Repr UTCTime

Equations

• Time.instReprUTCTime = { reprPrec := Time.reprUTCTime✝ }

instance Time.instBEqUTCTime : BEq UTCTime

Equations

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

instance Time.UTCTime.instToString : ToString UTCTime

Equations

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

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 }