structure Aesop.Nanos : Type

• nanos : Nat

def Aesop.instInhabitedNanos.default : Nanos

Equations

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

@[implicit_reducible]

instance Aesop.instInhabitedNanos : Inhabited Nanos

Equations

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

@[implicit_reducible]

instance Aesop.instBEqNanos : BEq Nanos

Equations

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

def Aesop.instBEqNanos.beq : Nanos → Nanos → Bool

Equations

• Aesop.instBEqNanos.beq { nanos := a } { nanos := b } = (a == b)
• Aesop.instBEqNanos.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Aesop.instOrdNanos : Ord Nanos

Equations

• Aesop.instOrdNanos = { compare := Aesop.instOrdNanos.ord }

def Aesop.instOrdNanos.ord : Nanos → Nanos → Ordering

Equations

• Aesop.instOrdNanos.ord { nanos := a } { nanos := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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₂ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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₂ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Aesop.Nanos.instAdd : Add Nanos

Equations

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

@[implicit_reducible]

instance Aesop.Nanos.instHDivNat : HDiv Nanos Nat Nanos

Equations

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

@[implicit_reducible]

instance Aesop.Nanos.instToJson : Lean.ToJson Nanos

Equations

• Aesop.Nanos.instToJson = { toJson := fun (x : Aesop.Nanos) => match x with | { nanos := n } => Lean.toJson n }

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

Equations

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