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

Equations

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

def UInt8.ofNatTruncate (n : Nat) : UInt8

Converts the given natural number to UInt8, but returns 2^8 - 1 for natural numbers >= 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

Equations

• Nat.toUInt8 = UInt8.ofNat

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) : Nat

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

Equations

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

def UInt16.ofNatTruncate (n : Nat) : UInt16

Converts the given natural number to UInt16, but returns 2^16 - 1 for natural numbers >= 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

Equations

• Nat.toUInt16 = UInt16.ofNat

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) : Nat

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) : UInt16

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

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

Pack a Nat less than 2^32 into a UInt32. This function is overridden with a native implementation.

Equations

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

def UInt32.ofNatTruncate (n : Nat) : UInt32

Converts the given natural number to UInt32, but returns 2^32 - 1 for natural numbers >= 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

Equations

• Nat.toUInt32 = UInt32.ofNat

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) : UInt16

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) : UInt32

Equations

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

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) : UInt32

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

Equations

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

def UInt64.ofNatTruncate (n : Nat) : UInt64

Converts the given natural number to UInt64, but returns 2^64 - 1 for natural numbers >= 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

Equations

• Nat.toUInt64 = UInt64.ofNat

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) : Nat

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) : UInt16

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) : UInt32

Equations

• a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) : UInt64

Equations

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

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) : UInt64

Equations

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

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) : UInt64

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

@[deprecated USize.size_pos (since := "2024-11-24")]

theorem usize_size_gt_zero : USize.size > 0

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

Equations

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

def USize.ofNatTruncate (n : Nat) : USize

Converts the given natural number to USize, but returns USize.size - 1 (i.e., 2^64 - 1 or 2^32 - 1 depending on the platform) for natural numbers >= 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

Equations

• Nat.toUSize = USize.ofNat

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) : Nat

Equations

• n.toNat = n.toBitVec.toNat

@[extern lean_usize_add]

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

Equations

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

@[extern lean_usize_sub]

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

Equations

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

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

Equations

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

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

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]

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

Equations

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

@[extern lean_usize_dec_le]

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

Equations

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

instance instDecidableLtUSize (a b : USize) : Decidable (a < b)

Equations

• instDecidableLtUSize a b = a.decLt b

instance instDecidableLeUSize (a b : USize) : Decidable (a ≤ b)

Equations

• instDecidableLeUSize a b = a.decLe b