structure Aesop.Nanos : Type

• nanos : Nat

Instances For

• Aesop.Nanos.instAdd
• Aesop.Nanos.instHDivNat
• Aesop.Nanos.instOfNat
• Aesop.instBEqNanos
• Aesop.instInhabitedNanos
• Aesop.instOrdNanos

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.instOfNat {n : Nat} : OfNat Aesop.Nanos n

Equations

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

instance Aesop.Nanos.instAdd : Add Aesop.Nanos

Equations

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

instance Aesop.Nanos.instHDivNat : HDiv Aesop.Nanos Nat Aesop.Nanos

Equations

• Aesop.Nanos.instHDivNat = { 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.