structure Time.UTCTime : Type

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

• utctDay : Time.Day
• utctDayTime : Time.DiffTime

instance Time.instReprUTCTime : Repr Time.UTCTime

Equations

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

instance Time.instBEqUTCTime : BEq Time.UTCTime

Equations

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

instance Time.UTCTime.instToString : ToString Time.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 : IO.FS.SystemTime) : Time.UTCTime

Equations

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

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

Equations

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

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

Equations

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

instance Time.UTCTime.instHSubDiffTime : HSub Time.UTCTime Time.UTCTime Time.DiffTime

Equations

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