Documentation

Time.Clock.SystemTime

source
@[extern lean_clock_gettime]
opaque Time.clock_gettime :
IO (Int × UInt32)
source
def Time.getSystemTime :
IO { t : IO.FS.SystemTime // t.nsec.toNat < 10 ^ 9 }

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance Time.instToStringSystemTime_time :
    ToString IO.FS.SystemTime
    Equations
    • One or more equations did not get rendered due to their size.