structure Aesop.Nanos : Type

• nanos : Nat

instance Aesop.instInhabitedNanos : Inhabited Aesop.Nanos

Equations

• Aesop.instInhabitedNanos = { default := { nanos := default } }

instance Aesop.instBEqNanos : BEq Aesop.Nanos

Equations

• Aesop.instBEqNanos = { beq := Aesop.beqNanos✝ }

instance Aesop.instOrdNanos : Ord Aesop.Nanos

Equations

• Aesop.instOrdNanos = { compare := Aesop.ordNanos✝ }

instance Aesop.Nanos.instOfNatNanos {n : Nat} : OfNat Aesop.Nanos n

Equations

• Aesop.Nanos.instOfNatNanos = { ofNat := { nanos := n } }

instance Aesop.Nanos.instAddNanos : Add Aesop.Nanos

Equations

• Aesop.Nanos.instAddNanos = { add := fun (n m : Aesop.Nanos) => { nanos := n.nanos + m.nanos } }

instance Aesop.Nanos.instHDivNanosNat : HDiv Aesop.Nanos Nat Aesop.Nanos

Equations

• Aesop.Nanos.instHDivNanosNat = { hDiv := fun (n : Aesop.Nanos) (m : Nat) => { nanos := n.nanos / m } }

def Aesop.Nanos.printAsMillis (n : Aesop.Nanos) : String

Equations

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