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 : Fixed Nano

def Time.instBEqDiffTime.beq : DiffTime → DiffTime → Bool

Equations

• Time.instBEqDiffTime.beq { val := a } { val := b } = (a == b)
• Time.instBEqDiffTime.beq x✝¹ x✝ = false

instance Time.instBEqDiffTime : BEq DiffTime

Equations

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

def Time.DiffTime.fromSecNsec (sign : Sign) (sec nsec : Nat) (h : nsec < 10 ^ 9) : DiffTime

Equations

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

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

Equations

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

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

Equations

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

instance Time.DiffTime.instToString : ToString DiffTime

Equations

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

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

Equations

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

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

Equations

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

instance Time.DiffTime.instSub : Sub DiffTime

Equations

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

instance Time.DiffTime.instAdd : Add DiffTime

Equations

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