structure Aesop.Nanos : Type

• nanos : Nat

instance Aesop.instInhabitedNanos : Inhabited Nanos

Equations

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

instance Aesop.instBEqNanos : BEq Nanos

Equations

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

instance Aesop.instOrdNanos : Ord Nanos

Equations

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

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

Equations

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

instance Aesop.Nanos.instLT : LT Nanos

Equations

• Aesop.Nanos.instLT = { lt := fun (x x_1 : Aesop.Nanos) => match x, x_1 with | { nanos := n₁ }, { nanos := n₂ } => n₁ < n₂ }

instance Aesop.Nanos.instDecidableRelLt : DecidableRel fun (x1 x2 : Nanos) => x1 < x2

Equations

• { nanos := n₂ }.instDecidableRelLt { nanos := n₂_1 } = inferInstanceAs (Decidable (n₂ < n₂_1))

instance Aesop.Nanos.instLE : LE Nanos

Equations

• Aesop.Nanos.instLE = { le := fun (x x_1 : Aesop.Nanos) => match x, x_1 with | { nanos := n₁ }, { nanos := n₂ } => n₁ ≤ n₂ }

instance Aesop.Nanos.instDecidableRelLe : DecidableRel fun (x1 x2 : Nanos) => x1 ≤ x2

Equations

• { nanos := n₂ }.instDecidableRelLe { nanos := n₂_1 } = inferInstanceAs (Decidable (n₂ ≤ n₂_1))

instance Aesop.Nanos.instAdd : Add Nanos

Equations

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

instance Aesop.Nanos.instHDivNat : HDiv Nanos Nat Nanos

Equations

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

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

Equations

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