def Time.Nano : Nat

digits of nano second

Equations

• Time.Nano = 9

structure Time.DiffTime : Type

This is a length of time in nsecs, as measured by a clock.

• val : Time.Fixed Time.Nano

instance Time.instReprDiffTime : Repr Time.DiffTime

Equations

• Time.instReprDiffTime = { reprPrec := Time.reprDiffTime✝ }

instance Time.instBEqDiffTime : BEq Time.DiffTime

Equations

• Time.instBEqDiffTime = { beq := Time.beqDiffTime✝ }

def Time.DiffTime.fromSecNsec (sign : Time.Sign) (sec : Nat) (nsec : Nat) : Time.DiffTime

Equations

• Time.DiffTime.fromSecNsec sign sec nsec = { val := Time.Fixed.toFixed sign sec (Time.Fixed.toDenominator nsec Time.Nano) }

def Time.DiffTime.fromSec (sec : Int) : Time.DiffTime

Equations

• Time.DiffTime.fromSec sec = { val := Time.Fixed.toFixed (Time.Fixed.toSign sec) sec.natAbs default }

def Time.DiffTime.toSec (dt : Time.DiffTime) : Int

Equations

• dt.toSec = let p := dt.val.toParts; match p.sign with | Time.Sign.Neg => -↑p.numerator | Time.Sign.Nonneg => ↑p.numerator

instance Time.DiffTime.instToString : ToString Time.DiffTime

Equations

• Time.DiffTime.instToString = { toString := fun (a : Time.DiffTime) => toString "" ++ toString a.val ++ toString "" }

def Time.DiffTime.sub (dt1 : Time.DiffTime) (dt2 : Time.DiffTime) : Time.DiffTime

Equations

• dt1.sub dt2 = { val := dt1.val - dt2.val }

def Time.DiffTime.add (dt1 : Time.DiffTime) (dt2 : Time.DiffTime) : Time.DiffTime

Equations

• dt1.add dt2 = { val := dt1.val + dt2.val }

instance Time.DiffTime.instSub : Sub Time.DiffTime

Equations

• Time.DiffTime.instSub = { sub := Time.DiffTime.sub }

instance Time.DiffTime.instAdd : Add Time.DiffTime

Equations

• Time.DiffTime.instAdd = { add := Time.DiffTime.add }