Documentation

Init.Data.UInt.BasicAux

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) :

Equations

x.val = x.toBitVec.toFin

@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) :

Equations

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

@[reducible, inline]

abbrev Nat.toUInt8 (n : Nat) :

Equations

Nat.toUInt8 = UInt8.ofNat

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) :

Equations

n.toNat = n.toBitVec.toNat

instance UInt8.instOfNat {n : Nat} :

Equations

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

def UInt16.val (x : UInt16) :

Equations

x.val = x.toBitVec.toFin

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) :

Equations

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

@[reducible, inline]

abbrev Nat.toUInt16 (n : Nat) :

Equations

Nat.toUInt16 = UInt16.ofNat

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) :

Equations

n.toNat = n.toBitVec.toNat

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) :

Equations

a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) :

Equations

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

instance UInt16.instOfNat {n : Nat} :

Equations

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

def UInt32.val (x : UInt32) :

Equations

x.val = x.toBitVec.toFin

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) :

Equations

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

@[extern lean_uint32_of_nat]

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

Equations

UInt32.ofNat' n h = { toBitVec := n#'h }

def UInt32.ofNatTruncate (n : Nat) :

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) :

Equations

Nat.toUInt32 = UInt32.ofNat

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) :

Equations

a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) :

Equations

a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) :

Equations

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

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) :

Equations

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

instance UInt32.instOfNat {n : Nat} :

Equations

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

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

n < m → ofNat' n h1 < ofNat m

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

m < n → ofNat m < ofNat' n h1

def UInt64.val (x : UInt64) :

Equations

x.val = x.toBitVec.toFin

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) :

Equations

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

@[reducible, inline]

abbrev Nat.toUInt64 (n : Nat) :

Equations

Nat.toUInt64 = UInt64.ofNat

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) :

Equations

n.toNat = n.toBitVec.toNat

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) :

Equations

a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) :

Equations

a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) :

Equations

a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) :

Equations

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

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) :

Equations

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

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) :

Equations

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

instance UInt64.instOfNat {n : Nat} :

Equations

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

@[deprecated usize_size_pos (since := "2024-11-24")]

theorem usize_size_gt_zero :

def USize.val (x : USize) :

Equations

x.val = x.toBitVec.toFin

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) :

Equations

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

@[reducible, inline]

abbrev Nat.toUSize (n : Nat) :

Equations

Nat.toUSize = USize.ofNat

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) :

Equations

n.toNat = n.toBitVec.toNat

@[extern lean_usize_add]

def USize.add (a b : USize) :

Equations

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

@[extern lean_usize_sub]

def USize.sub (a b : USize) :

Equations

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

def USize.lt (a b : USize) :

Equations

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

def USize.le (a b : USize) :

Equations

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

instance USize.instOfNat {n : Nat} :

Equations

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

instance instAddUSize :

Equations

instAddUSize = { add := USize.add }

instance instSubUSize :

Equations

instSubUSize = { sub := USize.sub }

instance instLTUSize :

Equations

instLTUSize = { lt := USize.lt }

instance instLEUSize :

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