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.val (x : UInt8) : Fin UInt8.size

Equations

• x.val = x.toBitVec.toFin

@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) : UInt8

Equations

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

@[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.val (x : UInt16) : Fin UInt16.size

Equations

• x.val = x.toBitVec.toFin

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) : UInt16

Equations

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

@[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.val (x : UInt32) : Fin UInt32.size

Equations

• x.val = x.toBitVec.toFin

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) : UInt32

Equations

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

@[extern lean_uint32_of_nat]

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

Equations

• UInt32.ofNat' n h = { toBitVec := 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.ofNat' n h else UInt32.ofNat' (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.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : n < m → UInt32.ofNat' n h1 < UInt32.ofNat m

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

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

Equations

• x.val = x.toBitVec.toFin

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) : UInt64

Equations

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

@[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_pos (since := "2024-11-24")]

theorem usize_size_gt_zero : USize.size > 0

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

Equations

• x.val = x.toBitVec.toFin

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) : USize

Equations

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

@[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