class Printf.Sign (a : Type u) : Type u

• sign : a → a

class Printf.Num (a : Type u) extends Add a, Sub a, Mul a, Div a, Ord a, LT a, LE a, BEq a : Type u

• add : a → a → a
• sub : a → a → a
• mul : a → a → a
• div : a → a → a
• compare : a → a → Ordering
• lt : a → a → Prop
• le : a → a → Prop
• beq : a → a → Bool

instance Printf.instNumNat : Num Nat

Equations

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

instance Printf.instNumInt : Num Int

Equations

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

instance Printf.instOrdFloat32_printf : Ord Float32

Equations

• Printf.instOrdFloat32_printf = { compare := fun (a b : Float32) => if (a == b) = true then Ordering.eq else if a < b then Ordering.lt else Ordering.gt }

instance Printf.instNumFloat32 : Num Float32

Equations

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

instance Printf.instOrdFloat_printf : Ord Float

Equations

• Printf.instOrdFloat_printf = { compare := fun (a b : Float) => if (a == b) = true then Ordering.eq else if a < b then Ordering.lt else Ordering.gt }

instance Printf.instNumFloat : Num Float

Equations

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