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

• ofInt : Int → a

instance Printf.instOfIntNat : OfInt Nat

Equations

• Printf.instOfIntNat = { ofInt := fun (x : Int) => x.toNat }

instance Printf.instOfIntInt : OfInt Int

Equations

• Printf.instOfIntInt = { ofInt := id }

instance Printf.instOfIntInt8 : OfInt Int8

Equations

• Printf.instOfIntInt8 = { ofInt := Int8.ofInt }

instance Printf.instOfIntInt16 : OfInt Int16

Equations

• Printf.instOfIntInt16 = { ofInt := Int16.ofInt }

instance Printf.instOfIntInt32 : OfInt Int32

Equations

• Printf.instOfIntInt32 = { ofInt := Int32.ofInt }

instance Printf.instOfIntInt64 : OfInt Int64

Equations

• Printf.instOfIntInt64 = { ofInt := Int64.ofInt }

instance Printf.instOfIntUInt8 : OfInt UInt8

Equations

• Printf.instOfIntUInt8 = { ofInt := UInt8.ofNat ∘ Int.toNat }

instance Printf.instOfIntUInt16 : OfInt UInt16

Equations

• Printf.instOfIntUInt16 = { ofInt := UInt16.ofNat ∘ Int.toNat }

instance Printf.instOfIntUInt32 : OfInt UInt32

Equations

• Printf.instOfIntUInt32 = { ofInt := UInt32.ofNat ∘ Int.toNat }

instance Printf.instOfIntUInt64 : OfInt UInt64

Equations

• Printf.instOfIntUInt64 = { ofInt := UInt64.ofNat ∘ Int.toNat }

instance Printf.instOfIntFloat32 : OfInt Float32

Equations

• Printf.instOfIntFloat32 = { ofInt := Float32.ofInt }

instance Printf.instOfIntFloat : OfInt Float

Equations

• Printf.instOfIntFloat = { ofInt := Float.ofInt }

class Printf.Integral (a : Type u) extends Printf.Num a, Zero a, Div a, Mod a, Printf.OfInt a, Ord a, LT a, BEq a, LE 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
• zero : a
• mod : a → a → a
• ofInt : Int → a
• toInt : a → Int

instance Printf.instIntegralNat : Integral Nat

Equations

• Printf.instIntegralNat = { toNum := Printf.instNumNat, toZero := Zero.ofOfNat0, toMod := Nat.instMod, toOfInt := Printf.instOfIntNat, toInt := Int.ofNat }

instance Printf.instIntegralInt : Integral Int

Equations

• Printf.instIntegralInt = { toNum := Printf.instNumInt, toZero := Zero.ofOfNat0, toMod := Int.instMod, toOfInt := Printf.instOfIntInt, toInt := id }

instance Printf.instIntegralInt8 : Integral Int8

Equations

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

instance Printf.instIntegralInt16 : Integral Int16

Equations

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

instance Printf.instIntegralInt32 : Integral Int32

Equations

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

instance Printf.instIntegralInt64 : Integral Int64

Equations

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

instance Printf.instIntegralUInt8 : Integral UInt8

Equations

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

instance Printf.instIntegralUInt16 : Integral UInt16

Equations

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

instance Printf.instIntegralUInt32 : Integral UInt32

Equations

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

instance Printf.instIntegralUInt64 : Integral UInt64

Equations

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

def Printf.fromIntegral {a b : Type u} [Integral a] [OfInt b] : a → b

Equations

• Printf.fromIntegral = Printf.OfInt.ofInt ∘ Printf.Integral.toInt

def Printf.divMod {n : Type u} [Div n] [Mod n] (a b : n) : n × n

Equations

• Printf.divMod a b = (a / b, a % b)

partial def Printf.itosb (b : Nat) (n : Int) : String