theorem UInt8.val_eq_of_lt {a : ℕ} : a < UInt8.size → ↑(UInt8.ofNat a).val = a

theorem UInt16.val_eq_of_lt {a : ℕ} : a < UInt16.size → ↑(UInt16.ofNat a).val = a

theorem UInt32.val_eq_of_lt {a : ℕ} : a < UInt32.size → ↑(UInt32.ofNat a).val = a

theorem UInt64.val_eq_of_lt {a : ℕ} : a < UInt64.size → ↑(UInt64.ofNat a).val = a

theorem USize.val_eq_of_lt {a : ℕ} : a < USize.size → ↑(USize.ofNat a).val = a

instance UInt8.neZero : NeZero UInt8.size

instance UInt16.neZero : NeZero UInt16.size

instance UInt32.neZero : NeZero UInt32.size

instance UInt64.neZero : NeZero UInt64.size

instance USize.neZero : NeZero USize.size

instance UInt16.instSMulNatUInt16 : SMul ℕ UInt16

theorem USize.intCast_def (z : ℤ) : ↑z = { val := ↑z }

theorem UInt8.val_eq_of_eq {a : UInt8} {b : UInt8} : a = b → a.val = b.val

theorem USize.eq_of_val_eq {a : USize} {b : USize} : a.val = b.val → a = b

instance USize.instPowUSizeNat : Pow USize ℕ

instance UInt32.instSMulNatUInt32 : SMul ℕ UInt32

theorem UInt32.one_def : 1 = { val := 1 }

theorem USize.add_def (a : USize) (b : USize) : a + b = { val := a.val + b.val }

theorem UInt64.neg_def (a : UInt64) : -a = { val := -a.val }

theorem UInt8.val_injective : Function.Injective UInt8.val

theorem UInt16.intCast_def (z : ℤ) : ↑z = { val := ↑z }

instance UInt16.instIntCastUInt16 : IntCast UInt16

instance UInt32.instSMulIntUInt32 : SMul ℤ UInt32

theorem UInt32.pow_def (a : UInt32) (n : ℕ) : a ^ n = { val := a.val ^ n }

instance UInt16.instCommRingUInt16 : CommRing UInt16

instance USize.instNegUSize : Neg USize

theorem UInt64.natCast_def (n : ℕ) : ↑n = { val := ↑n }

theorem USize.zsmul_def (z : ℤ) (a : USize) : z • a = { val := z • a.val }

theorem UInt8.mul_def (a : UInt8) (b : UInt8) : a * b = { val := a.val * b.val }

theorem USize.zero_def : 0 = { val := 0 }

theorem UInt32.val_injective : Function.Injective UInt32.val

instance UInt32.instIntCastUInt32 : IntCast UInt32

instance USize.instSMulNatUSize : SMul ℕ USize

instance UInt64.instCommRingUInt64 : CommRing UInt64

instance USize.instSMulIntUSize : SMul ℤ USize

theorem USize.val_injective : Function.Injective USize.val

theorem UInt8.intCast_def (z : ℤ) : ↑z = { val := ↑z }

theorem USize.natCast_def (n : ℕ) : ↑n = { val := ↑n }

theorem USize.pow_def (a : USize) (n : ℕ) : a ^ n = { val := a.val ^ n }

theorem UInt16.neg_def (a : UInt16) : -a = { val := -a.val }

theorem UInt16.one_def : 1 = { val := 1 }

theorem UInt32.sub_def (a : UInt32) (b : UInt32) : a - b = { val := a.val - b.val }

theorem UInt64.intCast_def (z : ℤ) : ↑z = { val := ↑z }

@[simp]

theorem USize.mk_val_eq (a : USize) : { val := a.val } = a

instance UInt64.instIntCastUInt64 : IntCast UInt64

theorem UInt8.one_def : 1 = { val := 1 }

theorem UInt8.eq_of_val_eq {a : UInt8} {b : UInt8} : a.val = b.val → a = b

@[simp]

theorem UInt32.mk_val_eq (a : UInt32) : { val := a.val } = a

instance UInt32.instCommRingUInt32 : CommRing UInt32

instance UInt32.instNatCastUInt32 : NatCast UInt32

instance UInt8.instSMulIntUInt8 : SMul ℤ UInt8

theorem UInt8.neg_def (a : UInt8) : -a = { val := -a.val }

instance UInt64.instSMulIntUInt64 : SMul ℤ UInt64

instance UInt64.instPowUInt64Nat : Pow UInt64 ℕ

theorem UInt8.zsmul_def (z : ℤ) (a : UInt8) : z • a = { val := z • a.val }

instance UInt8.instNegUInt8 : Neg UInt8

theorem UInt32.intCast_def (z : ℤ) : ↑z = { val := ↑z }

theorem UInt8.pow_def (a : UInt8) (n : ℕ) : a ^ n = { val := a.val ^ n }

instance USize.instInhabitedUSize : Inhabited USize

theorem UInt8.mod_def (a : UInt8) (b : UInt8) : a % b = { val := a.val % b.val }

theorem UInt16.sub_def (a : UInt16) (b : UInt16) : a - b = { val := a.val - b.val }

theorem UInt64.one_def : 1 = { val := 1 }

@[simp]

theorem UInt64.mk_val_eq (a : UInt64) : { val := a.val } = a

theorem USize.mul_def (a : USize) (b : USize) : a * b = { val := a.val * b.val }

theorem UInt32.natCast_def (n : ℕ) : ↑n = { val := ↑n }

theorem USize.mod_def (a : USize) (b : USize) : a % b = { val := a.val % b.val }

theorem UInt32.zsmul_def (z : ℤ) (a : UInt32) : z • a = { val := z • a.val }

instance USize.instIntCastUSize : IntCast USize

theorem UInt16.add_def (a : UInt16) (b : UInt16) : a + b = { val := a.val + b.val }

theorem UInt64.pow_def (a : UInt64) (n : ℕ) : a ^ n = { val := a.val ^ n }

theorem UInt16.mul_def (a : UInt16) (b : UInt16) : a * b = { val := a.val * b.val }

theorem UInt8.nsmul_def (n : ℕ) (a : UInt8) : n • a = { val := n • a.val }

theorem UInt16.nsmul_def (n : ℕ) (a : UInt16) : n • a = { val := n • a.val }

instance UInt64.instNegUInt64 : Neg UInt64

theorem UInt64.mod_def (a : UInt64) (b : UInt64) : a % b = { val := a.val % b.val }

instance UInt16.instSMulIntUInt16 : SMul ℤ UInt16

theorem UInt64.zsmul_def (z : ℤ) (a : UInt64) : z • a = { val := z • a.val }

instance UInt16.instNegUInt16 : Neg UInt16

theorem UInt64.sub_def (a : UInt64) (b : UInt64) : a - b = { val := a.val - b.val }

theorem UInt32.val_eq_of_eq {a : UInt32} {b : UInt32} : a = b → a.val = b.val

@[simp]

theorem UInt8.mk_val_eq (a : UInt8) : { val := a.val } = a

theorem UInt8.sub_def (a : UInt8) (b : UInt8) : a - b = { val := a.val - b.val }

instance UInt64.instInhabitedUInt64 : Inhabited UInt64

theorem USize.nsmul_def (n : ℕ) (a : USize) : n • a = { val := n • a.val }

theorem UInt16.val_injective : Function.Injective UInt16.val

@[simp]

theorem UInt16.mk_val_eq (a : UInt16) : { val := a.val } = a

instance USize.instCommRingUSize : CommRing USize

instance UInt8.instPowUInt8Nat : Pow UInt8 ℕ

theorem USize.neg_def (a : USize) : -a = { val := -a.val }

theorem UInt64.val_injective : Function.Injective UInt64.val

instance UInt8.instSMulNatUInt8 : SMul ℕ UInt8

theorem UInt64.nsmul_def (n : ℕ) (a : UInt64) : n • a = { val := n • a.val }

theorem UInt16.val_eq_of_eq {a : UInt16} {b : UInt16} : a = b → a.val = b.val

theorem UInt32.add_def (a : UInt32) (b : UInt32) : a + b = { val := a.val + b.val }

theorem UInt32.eq_of_val_eq {a : UInt32} {b : UInt32} : a.val = b.val → a = b

theorem UInt32.neg_def (a : UInt32) : -a = { val := -a.val }

instance UInt16.instPowUInt16Nat : Pow UInt16 ℕ

instance UInt32.instNegUInt32 : Neg UInt32

theorem USize.one_def : 1 = { val := 1 }

theorem UInt64.zero_def : 0 = { val := 0 }

theorem UInt16.zero_def : 0 = { val := 0 }

theorem UInt16.natCast_def (n : ℕ) : ↑n = { val := ↑n }

theorem UInt32.mod_def (a : UInt32) (b : UInt32) : a % b = { val := a.val % b.val }

theorem UInt64.val_eq_of_eq {a : UInt64} {b : UInt64} : a = b → a.val = b.val

theorem UInt64.mul_def (a : UInt64) (b : UInt64) : a * b = { val := a.val * b.val }

theorem UInt32.zero_def : 0 = { val := 0 }

theorem USize.val_eq_of_eq {a : USize} {b : USize} : a = b → a.val = b.val

theorem UInt16.mod_def (a : UInt16) (b : UInt16) : a % b = { val := a.val % b.val }

theorem UInt8.natCast_def (n : ℕ) : ↑n = { val := ↑n }

theorem UInt64.eq_of_val_eq {a : UInt64} {b : UInt64} : a.val = b.val → a = b

instance UInt64.instSMulNatUInt64 : SMul ℕ UInt64

instance UInt16.instNatCastUInt16 : NatCast UInt16

instance UInt64.instNatCastUInt64 : NatCast UInt64

instance UInt8.instNatCastUInt8 : NatCast UInt8

theorem UInt32.mul_def (a : UInt32) (b : UInt32) : a * b = { val := a.val * b.val }

instance UInt32.instInhabitedUInt32 : Inhabited UInt32

instance USize.instNatCastUSize : NatCast USize

theorem USize.sub_def (a : USize) (b : USize) : a - b = { val := a.val - b.val }

theorem UInt8.zero_def : 0 = { val := 0 }

instance UInt16.instInhabitedUInt16 : Inhabited UInt16

theorem UInt16.eq_of_val_eq {a : UInt16} {b : UInt16} : a.val = b.val → a = b

instance UInt32.instPowUInt32Nat : Pow UInt32 ℕ

instance UInt8.instInhabitedUInt8 : Inhabited UInt8

theorem UInt32.nsmul_def (n : ℕ) (a : UInt32) : n • a = { val := n • a.val }

instance UInt8.instCommRingUInt8 : CommRing UInt8

instance UInt8.instIntCastUInt8 : IntCast UInt8

theorem UInt64.add_def (a : UInt64) (b : UInt64) : a + b = { val := a.val + b.val }

theorem UInt16.zsmul_def (z : ℤ) (a : UInt16) : z • a = { val := z • a.val }

theorem UInt16.pow_def (a : UInt16) (n : ℕ) : a ^ n = { val := a.val ^ n }

theorem UInt8.add_def (a : UInt8) (b : UInt8) : a + b = { val := a.val + b.val }

def UInt8.isUpper (c : UInt8) : Bool

Is this an uppercase ASCII letter?

def UInt8.isLower (c : UInt8) : Bool

Is this a lowercase ASCII letter?

def UInt8.isAlpha (c : UInt8) : Bool

Is this an alphabetic ASCII character?

def UInt8.isDigit (c : UInt8) : Bool

Is this an ASCII digit character?

def UInt8.isAlphanum (c : UInt8) : Bool

Is this an alphanumeric ASCII character?

theorem UInt8.toChar_aux (n : ℕ) (h : n < UInt8.size) : Nat.isValidChar ↑(UInt32.ofNat n).val

def UInt8.toChar (n : UInt8) : Char

The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.