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

Equations

• UInt8.neZero = (_ : NeZero UInt8.size)

instance UInt16.neZero : NeZero UInt16.size

Equations

• UInt16.neZero = (_ : NeZero UInt16.size)

instance UInt32.neZero : NeZero UInt32.size

Equations

• UInt32.neZero = (_ : NeZero UInt32.size)

instance UInt64.neZero : NeZero UInt64.size

Equations

• UInt64.neZero = (_ : NeZero UInt64.size)

instance USize.neZero : NeZero USize.size

Equations

• USize.neZero = (_ : NeZero USize.size)

instance UInt16.instSMulNatUInt16 : SMul ℕ UInt16

Equations

• UInt16.instSMulNatUInt16 = { smul := fun (n : ℕ) (a : UInt16) => { val := n • a.val } }

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 ℕ

Equations

• USize.instPowUSizeNat = { pow := fun (a : USize) (n : ℕ) => { val := a.val ^ n } }

instance UInt32.instSMulNatUInt32 : SMul ℕ UInt32

Equations

• UInt32.instSMulNatUInt32 = { smul := fun (n : ℕ) (a : UInt32) => { val := n • a.val } }

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

Equations

• UInt16.instIntCastUInt16 = { intCast := fun (z : ℤ) => { val := ↑z } }

instance UInt32.instSMulIntUInt32 : SMul ℤ UInt32

Equations

• UInt32.instSMulIntUInt32 = { smul := fun (z : ℤ) (a : UInt32) => { val := z • a.val } }

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

instance UInt16.instCommRingUInt16 : CommRing UInt16

Equations

• One or more equations did not get rendered due to their size.

instance USize.instNegUSize : Neg USize

Equations

• USize.instNegUSize = { neg := fun (a : USize) => { val := -a.val } }

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

Equations

• UInt32.instIntCastUInt32 = { intCast := fun (z : ℤ) => { val := ↑z } }

instance USize.instSMulNatUSize : SMul ℕ USize

Equations

• USize.instSMulNatUSize = { smul := fun (n : ℕ) (a : USize) => { val := n • a.val } }

instance UInt64.instCommRingUInt64 : CommRing UInt64

Equations

• One or more equations did not get rendered due to their size.

instance USize.instSMulIntUSize : SMul ℤ USize

Equations

• USize.instSMulIntUSize = { smul := fun (z : ℤ) (a : USize) => { val := z • a.val } }

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

Equations

• UInt64.instIntCastUInt64 = { intCast := fun (z : ℤ) => { val := ↑z } }

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

Equations

• One or more equations did not get rendered due to their size.

instance UInt32.instNatCastUInt32 : NatCast UInt32

Equations

• UInt32.instNatCastUInt32 = { natCast := fun (n : ℕ) => { val := ↑n } }

instance UInt8.instSMulIntUInt8 : SMul ℤ UInt8

Equations

• UInt8.instSMulIntUInt8 = { smul := fun (z : ℤ) (a : UInt8) => { val := z • a.val } }

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

instance UInt64.instSMulIntUInt64 : SMul ℤ UInt64

Equations

• UInt64.instSMulIntUInt64 = { smul := fun (z : ℤ) (a : UInt64) => { val := z • a.val } }

instance UInt64.instPowUInt64Nat : Pow UInt64 ℕ

Equations

• UInt64.instPowUInt64Nat = { pow := fun (a : UInt64) (n : ℕ) => { val := a.val ^ n } }

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

instance UInt8.instNegUInt8 : Neg UInt8

Equations

• UInt8.instNegUInt8 = { neg := fun (a : UInt8) => { val := -a.val } }

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

Equations

• USize.instInhabitedUSize = { default := 0 }

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

Equations

• USize.instIntCastUSize = { intCast := fun (z : ℤ) => { val := ↑z } }

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

Equations

• UInt64.instNegUInt64 = { neg := fun (a : UInt64) => { val := -a.val } }

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

instance UInt16.instSMulIntUInt16 : SMul ℤ UInt16

Equations

• UInt16.instSMulIntUInt16 = { smul := fun (z : ℤ) (a : UInt16) => { val := z • a.val } }

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

instance UInt16.instNegUInt16 : Neg UInt16

Equations

• UInt16.instNegUInt16 = { neg := fun (a : UInt16) => { val := -a.val } }

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

Equations

• UInt64.instInhabitedUInt64 = { default := 0 }

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

Equations

• One or more equations did not get rendered due to their size.

instance UInt8.instPowUInt8Nat : Pow UInt8 ℕ

Equations

• UInt8.instPowUInt8Nat = { pow := fun (a : UInt8) (n : ℕ) => { val := a.val ^ n } }

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

theorem UInt64.val_injective : Function.Injective UInt64.val

instance UInt8.instSMulNatUInt8 : SMul ℕ UInt8

Equations

• UInt8.instSMulNatUInt8 = { smul := fun (n : ℕ) (a : UInt8) => { val := n • a.val } }

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 ℕ

Equations

• UInt16.instPowUInt16Nat = { pow := fun (a : UInt16) (n : ℕ) => { val := a.val ^ n } }

instance UInt32.instNegUInt32 : Neg UInt32

Equations

• UInt32.instNegUInt32 = { neg := fun (a : UInt32) => { val := -a.val } }

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

Equations

• UInt64.instSMulNatUInt64 = { smul := fun (n : ℕ) (a : UInt64) => { val := n • a.val } }

instance UInt16.instNatCastUInt16 : NatCast UInt16

Equations

• UInt16.instNatCastUInt16 = { natCast := fun (n : ℕ) => { val := ↑n } }

instance UInt64.instNatCastUInt64 : NatCast UInt64

Equations

• UInt64.instNatCastUInt64 = { natCast := fun (n : ℕ) => { val := ↑n } }

instance UInt8.instNatCastUInt8 : NatCast UInt8

Equations

• UInt8.instNatCastUInt8 = { natCast := fun (n : ℕ) => { val := ↑n } }

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

instance UInt32.instInhabitedUInt32 : Inhabited UInt32

Equations

• UInt32.instInhabitedUInt32 = { default := 0 }

instance USize.instNatCastUSize : NatCast USize

Equations

• USize.instNatCastUSize = { natCast := fun (n : ℕ) => { val := ↑n } }

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

Equations

• UInt16.instInhabitedUInt16 = { default := 0 }

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

instance UInt32.instPowUInt32Nat : Pow UInt32 ℕ

Equations

• UInt32.instPowUInt32Nat = { pow := fun (a : UInt32) (n : ℕ) => { val := a.val ^ n } }

instance UInt8.instInhabitedUInt8 : Inhabited UInt8

Equations

• UInt8.instInhabitedUInt8 = { default := 0 }

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

instance UInt8.instCommRingUInt8 : CommRing UInt8

Equations

• One or more equations did not get rendered due to their size.

instance UInt8.instIntCastUInt8 : IntCast UInt8

Equations

• UInt8.instIntCastUInt8 = { intCast := fun (z : ℤ) => { val := ↑z } }

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?

Equations

• UInt8.isUpper c = (decide (c ≥ 65) && decide (c ≤ 90))

def UInt8.isLower (c : UInt8) : Bool

Is this a lowercase ASCII letter?

Equations

• UInt8.isLower c = (decide (c ≥ 97) && decide (c ≤ 122))

def UInt8.isAlpha (c : UInt8) : Bool

Is this an alphabetic ASCII character?

Equations

• UInt8.isAlpha c = (UInt8.isUpper c || UInt8.isLower c)

def UInt8.isDigit (c : UInt8) : Bool

Is this an ASCII digit character?

Equations

• UInt8.isDigit c = (decide (c ≥ 48) && decide (c ≤ 57))

def UInt8.isAlphanum (c : UInt8) : Bool

Is this an alphanumeric ASCII character?

Equations

• UInt8.isAlphanum c = (UInt8.isAlpha c || UInt8.isDigit c)

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.

Equations

• UInt8.toChar n = { val := UInt8.toUInt32 n, valid := (_ : Nat.isValidChar ↑(UInt32.ofNat ↑n.val).val) }