This module exists to provide the very basic UInt8 etc. definitions required for Init.Data.Char.Basic and Init.Data.Array.Basic. These are very important as they are used in meta code that is then (transitively) used in Init.Data.UInt.Basic and Init.Data.BitVec.Basic. This file thus breaks the import cycle that would be created by this dependency.

def UInt8.toFin (x : UInt8) : Fin size

Converts a UInt8 into the corresponding Fin UInt8.size.

Equations

• x.toFin = x.toBitVec.toFin

@[deprecated UInt8.toFin (since := "2025-02-12")]

def UInt8.val (x : UInt8) : Fin size

Converts a UInt8 into the corresponding Fin UInt8.size.

Equations

• x.val = x.toFin

@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) : UInt8

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• UInt8.ofNat 5 = 5
• UInt8.ofNat 255 = 255
• UInt8.ofNat 256 = 0
• UInt8.ofNat 259 = 3
• UInt8.ofNat 32770 = 2

Equations

• UInt8.ofNat n = { toBitVec := BitVec.ofNat 8 n }

def UInt8.ofNatTruncate (n : Nat) : UInt8

Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if the number is too large.

Returns 2^8 - 1 for natural numbers greater than or equal to 2^8.

Equations

• UInt8.ofNatTruncate n = if h : n < UInt8.size then UInt8.ofNatLT n h else UInt8.ofNatLT (UInt8.size - 1) UInt8.ofNatTruncate._proof_1

@[reducible, inline]

abbrev Nat.toUInt8 (n : Nat) : UInt8

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt8 5 = 5
• Nat.toUInt8 255 = 255
• Nat.toUInt8 256 = 0
• Nat.toUInt8 259 = 3
• Nat.toUInt8 32770 = 2

Equations

• Nat.toUInt8 = UInt8.ofNat

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) : Nat

Converts an 8-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

Equations

• n.toNat = n.toBitVec.toNat

instance UInt8.instOfNat {n : Nat} : OfNat UInt8 n

Equations

• UInt8.instOfNat = { ofNat := UInt8.ofNat n }

def UInt16.toFin (x : UInt16) : Fin size

Converts a UInt16 into the corresponding Fin UInt16.size.

Equations

• x.toFin = x.toBitVec.toFin

@[deprecated UInt16.toFin (since := "2025-02-12")]

def UInt16.val (x : UInt16) : Fin size

Converts a UInt16 into the corresponding Fin UInt16.size.

Equations

• x.val = x.toFin

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) : UInt16

Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• UInt16.ofNat 5 = 5
• UInt16.ofNat 255 = 255
• UInt16.ofNat 32770 = 32770
• UInt16.ofNat 65537 = 1

Equations

• UInt16.ofNat n = { toBitVec := BitVec.ofNat 16 n }

def UInt16.ofNatTruncate (n : Nat) : UInt16

Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if the number is too large.

Returns 2^16 - 1 for natural numbers greater than or equal to 2^16.

Equations

• UInt16.ofNatTruncate n = if h : n < UInt16.size then UInt16.ofNatLT n h else UInt16.ofNatLT (UInt16.size - 1) UInt16.ofNatTruncate._proof_1

@[reducible, inline]

abbrev Nat.toUInt16 (n : Nat) : UInt16

Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt16 5 = 5
• Nat.toUInt16 255 = 255
• Nat.toUInt16 32770 = 32770
• Nat.toUInt16 65537 = 1

Equations

• Nat.toUInt16 = UInt16.ofNat

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) : Nat

Converts a 16-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) : UInt8

Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) : UInt16

Converts 8-bit unsigned integers to 16-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt16 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

instance UInt16.instOfNat {n : Nat} : OfNat UInt16 n

Equations

• UInt16.instOfNat = { ofNat := UInt16.ofNat n }

def UInt32.toFin (x : UInt32) : Fin size

Converts a UInt32 into the corresponding Fin UInt32.size.

Equations

• x.toFin = x.toBitVec.toFin

@[deprecated UInt32.toFin (since := "2025-02-12")]

def UInt32.val (x : UInt32) : Fin size

Converts a UInt32 into the corresponding Fin UInt32.size.

Equations

• x.val = x.toFin

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) : UInt32

Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• UInt32.ofNat 5 = 5
• UInt32.ofNat 65539 = 65539
• UInt32.ofNat 4_294_967_299 = 3

Equations

• UInt32.ofNat n = { toBitVec := BitVec.ofNat 32 n }

@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13")]

def UInt32.ofNat' (n : Nat) (h : n < size) : UInt32

Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small enough to be representable without overflow; it must be smaller than 2^32.

This function is overridden at runtime with an efficient implementation.

Equations

• UInt32.ofNat' n h = UInt32.ofNatLT n h

def UInt32.ofNatTruncate (n : Nat) : UInt32

Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if the number is too large.

Returns 2^32 - 1 for natural numbers greater than or equal to 2^32.

Equations

• UInt32.ofNatTruncate n = if h : n < UInt32.size then UInt32.ofNatLT n h else UInt32.ofNatLT (UInt32.size - 1) UInt32.ofNatTruncate._proof_1

@[reducible, inline]

abbrev Nat.toUInt32 (n : Nat) : UInt32

Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt32 5 = 5
• Nat.toUInt32 65_539 = 65_539
• Nat.toUInt32 4_294_967_299 = 3

Equations

• Nat.toUInt32 = UInt32.ofNat

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) : UInt8

Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) : UInt16

Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) : UInt32

Converts 8-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt32 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) : UInt32

Converts 16-bit unsigned integers to 32-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt32 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

instance UInt32.instOfNat {n : Nat} : OfNat UInt32 n

Equations

• UInt32.instOfNat = { ofNat := UInt32.ofNat n }

theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) : n < m → ofNatLT n h1 < ofNat m

@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]

theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) : n < m → ofNatLT n h1 < ofNat m

theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) : m < n → ofNat m < ofNatLT n h1

@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]

theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < size) (h2 : m < size) : m < n → ofNat m < ofNatLT n h1

def UInt64.toFin (x : UInt64) : Fin size

Converts a UInt64 into the corresponding Fin UInt64.size.

Equations

• x.toFin = x.toBitVec.toFin

@[deprecated UInt64.toFin (since := "2025-02-12")]

def UInt64.val (x : UInt64) : Fin size

Converts a UInt64 into the corresponding Fin UInt64.size.

Equations

• x.val = x.toFin

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) : UInt64

Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• UInt64.ofNat 5 = 5
• UInt64.ofNat 65539 = 65539
• UInt64.ofNat 4_294_967_299 = 4_294_967_299
• UInt64.ofNat 18_446_744_073_709_551_620 = 4

Equations

• UInt64.ofNat n = { toBitVec := BitVec.ofNat 64 n }

def UInt64.ofNatTruncate (n : Nat) : UInt64

Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if the number is too large.

Returns 2^64 - 1 for natural numbers greater than or equal to 2^64.

Equations

• UInt64.ofNatTruncate n = if h : n < UInt64.size then UInt64.ofNatLT n h else UInt64.ofNatLT (UInt64.size - 1) UInt64.ofNatTruncate._proof_1

@[reducible, inline]

abbrev Nat.toUInt64 (n : Nat) : UInt64

Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt64 5 = 5
• Nat.toUInt64 65539 = 65539
• Nat.toUInt64 4_294_967_299 = 4_294_967_299
• Nat.toUInt64 18_446_744_073_709_551_620 = 4

Equations

• Nat.toUInt64 = UInt64.ofNat

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) : Nat

Converts a 64-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) : UInt8

Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) : UInt16

Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) : UInt32

Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) : UInt64

Converts 8-bit unsigned integers to 64-bit unsigned integers.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt64 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) : UInt64

Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt64 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) : UInt64

Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• a.toUInt64 = { toBitVec := { toFin := ⟨a.toNat, ⋯⟩ } }

instance UInt64.instOfNat {n : Nat} : OfNat UInt64 n

Equations

• UInt64.instOfNat = { ofNat := UInt64.ofNat n }

@[deprecated USize.size_eq (since := "2025-02-24")]

theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616

@[deprecated USize.size_pos (since := "2025-02-24")]

theorem usize_size_pos : 0 < USize.size

def USize.toFin (x : USize) : Fin size

Converts a USize into the corresponding Fin USize.size.

Equations

• x.toFin = x.toBitVec.toFin

@[deprecated USize.toFin (since := "2025-02-12")]

def USize.val (x : USize) : Fin size

Converts a USize into the corresponding Fin USize.size.

Equations

• x.val = x.toFin

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) : USize

Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• USize.ofNat n = { toBitVec := BitVec.ofNat System.Platform.numBits n }

def USize.ofNatTruncate (n : Nat) : USize

Converts a natural number to USize, returning the largest representable value if the number is too large.

Returns USize.size - 1, which is 2^64 - 1 or 2^32 - 1 depending on the platform, for natural numbers greater than or equal to USize.size.

Equations

• USize.ofNatTruncate n = if h : n < USize.size then USize.ofNatLT n h else USize.ofNatLT (USize.size - 1) USize.ofNatTruncate._proof_1

@[reducible, inline]

abbrev Nat.toUSize (n : Nat) : USize

Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Equations

• Nat.toUSize = USize.ofNat

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) : Nat

Converts a word-sized unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_usize_add]

def USize.add (a b : USize) : USize

Adds two word-sized unsigned integers, wrapping around on overflow. Usually accessed via the + operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.add b = { toBitVec := a.toBitVec + b.toBitVec }

@[extern lean_usize_sub]

def USize.sub (a b : USize) : USize

Subtracts one word-sized-bit unsigned integer from another, wrapping around on underflow. Usually accessed via the - operator.

This function is overridden at runtime with an efficient implementation.

Equations

• a.sub b = { toBitVec := a.toBitVec - b.toBitVec }

def USize.lt (a b : USize) : Prop

Strict inequality of word-sized unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the < operator.

Equations

• a.lt b = (a.toBitVec < b.toBitVec)

def USize.le (a b : USize) : Prop

Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding natural numbers. Usually accessed via the ≤ operator.

Equations

• a.le b = (a.toBitVec ≤ b.toBitVec)

instance USize.instOfNat {n : Nat} : OfNat USize n

Equations

• USize.instOfNat = { ofNat := USize.ofNat n }

instance instAddUSize : Add USize

Equations

• instAddUSize = { add := USize.add }

instance instSubUSize : Sub USize

Equations

• instSubUSize = { sub := USize.sub }

instance instLTUSize : LT USize

Equations

• instLTUSize = { lt := USize.lt }

instance instLEUSize : LE USize

Equations

• instLEUSize = { le := USize.le }

@[extern lean_usize_dec_lt]

instance USize.decLt (a b : USize) : Decidable (a < b)

Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via the DecidableLT USize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if (6 : USize) < 7 then "yes" else "no") = "yes"
• (if (5 : USize) < 5 then "yes" else "no") = "no"
• show ¬((7 : USize) < 7) by decide

Equations

• a.decLt b = inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))

@[extern lean_usize_dec_le]

instance USize.decLe (a b : USize) : Decidable (a ≤ b)

Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed via the DecidableLE USize instance.

This function is overridden at runtime with an efficient implementation.

Examples:

• (if (15 : USize) ≤ 15 then "yes" else "no") = "yes"
• (if (15 : USize) ≤ 5 then "yes" else "no") = "no"
• (if (5 : USize) ≤ 15 then "yes" else "no") = "yes"
• show (7 : USize) ≤ 7 by decide

Equations

• a.decLe b = inferInstanceAs (Decidable (a.toBitVec ≤ b.toBitVec))