@[extern lean_clock_gettime]

opaque Time.clock_gettime : IO (Int × UInt32)

def Time.getSystemTime : IO IO.FS.SystemTime

Get the system time, epoch start of 1970 UTC, leap-seconds ignored.

Equations

• Time.getSystemTime = do let tuple ← Time.clock_gettime pure { sec := tuple.fst, nsec := tuple.snd }

instance Time.instToStringSystemTime_time : ToString IO.FS.SystemTime

Equations

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