Documentation

Aesop.Nanos

structure Aesop.Nanos :

nanos : Nat

Instances For

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.instLT :

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 : Aesop.Nanos) => x1 < x2

Equations

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

instance Aesop.Nanos.instLE :

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 : Aesop.Nanos) => x1 ≤ x2

Equations

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

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) :

Equations

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