Adds Mathlib specific instances to the UIntX data types.

The CommRing instances (and the NatCast and IntCast instances from which they is built) are scoped in the UIntX.CommRing namespace, rather than available globally. As a result, the ring tactic will not work on UIntX types without open scoped UIntX.Ring.

This is because the presence of these casting operations contradicts assumptions made by the expression tree elaborator, namely that coercions do not form a cycle.

The UInt version also interferes more with software-verification use-cases, which is reason to be more cautious here.

instance USize.instNonUnitalCommRing : NonUnitalCommRing USize

Equations

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

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

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

instance UInt32.instNonUnitalCommRing : NonUnitalCommRing UInt32

Equations

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

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

instance UInt16.instPowNat_mathlib : Pow UInt16 ℕ

Equations

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

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

def UInt32.instNatCast : NatCast UInt32

To use this instance, use open scoped UInt32.CommRing.

See the module docstring for an explanation

Equations

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

instance UInt16.instCommMonoid : CommMonoid UInt16

Equations

• UInt16.instCommMonoid = Function.Injective.commMonoid UInt16.val UInt16.val_injective UInt16.instCommMonoid.proof_1 UInt16.instCommMonoid.proof_2 UInt16.instCommMonoid.proof_3

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

instance UInt64.instPowNat_mathlib : Pow UInt64 ℕ

Equations

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

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

instance UInt32.instNeg_mathlib : Neg UInt32

Equations

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

instance UInt64.instNeg_mathlib : Neg UInt64

Equations

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

theorem UInt16.val_injective : Function.Injective UInt16.val

instance UInt32.instCommMonoid : CommMonoid UInt32

Equations

• UInt32.instCommMonoid = Function.Injective.commMonoid UInt32.val UInt32.val_injective UInt32.instCommMonoid.proof_1 UInt32.instCommMonoid.proof_2 UInt32.instCommMonoid.proof_3

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

def UInt32.instIntCast : IntCast UInt32

To use this instance, use open scoped UInt32.CommRing.

See the module docstring for an explanation

Equations

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

instance UInt8.instCommMonoid : CommMonoid UInt8

Equations

• UInt8.instCommMonoid = Function.Injective.commMonoid UInt8.val UInt8.val_injective UInt8.instCommMonoid.proof_1 UInt8.instCommMonoid.proof_2 UInt8.instCommMonoid.proof_3

instance UInt32.instSMulNat : SMul ℕ UInt32

Equations

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

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

instance USize.instPowNat_mathlib : Pow USize ℕ

Equations

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

def UInt32.instCommRing : CommRing UInt32

To use this instance, use open scoped UInt32.CommRing.

See the module docstring for an explanation

Equations

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

def UInt64.instCommRing : CommRing UInt64

To use this instance, use open scoped UInt64.CommRing.

See the module docstring for an explanation

Equations

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

instance UInt64.instSMulNat : SMul ℕ UInt64

Equations

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

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

instance UInt16.instNonUnitalCommRing : NonUnitalCommRing UInt16

Equations

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

instance UInt16.instNeg_mathlib : Neg UInt16

Equations

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

instance UInt16.instSMulInt : SMul ℤ UInt16

Equations

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

def UInt16.instNatCast : NatCast UInt16

To use this instance, use open scoped UInt16.CommRing.

See the module docstring for an explanation

Equations

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

def UInt64.instIntCast : IntCast UInt64

To use this instance, use open scoped UInt64.CommRing.

See the module docstring for an explanation

Equations

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

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

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

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

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

instance UInt8.instNonUnitalCommRing : NonUnitalCommRing UInt8

Equations

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

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

def UInt8.instIntCast : IntCast UInt8

To use this instance, use open scoped UInt8.CommRing.

See the module docstring for an explanation

Equations

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

instance UInt16.instSMulNat : SMul ℕ UInt16

Equations

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

instance UInt32.neZero : NeZero UInt32.size

Equations

• UInt32.neZero = ⋯

instance UInt64.neZero : NeZero UInt64.size

Equations

• UInt64.neZero = ⋯

instance USize.instSMulInt : SMul ℤ USize

Equations

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

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

theorem UInt64.val_injective : Function.Injective UInt64.val

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

def USize.instCommRing : CommRing USize

To use this instance, use open scoped USize.CommRing.

See the module docstring for an explanation

Equations

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

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

theorem USize.val_injective : Function.Injective USize.val

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

def UInt8.instNatCast : NatCast UInt8

To use this instance, use open scoped UInt8.CommRing.

See the module docstring for an explanation

Equations

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

instance UInt64.instNonUnitalCommRing : NonUnitalCommRing UInt64

Equations

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

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

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

instance UInt64.instCommMonoid : CommMonoid UInt64

Equations

• UInt64.instCommMonoid = Function.Injective.commMonoid UInt64.val UInt64.val_injective UInt64.instCommMonoid.proof_1 UInt64.instCommMonoid.proof_2 UInt64.instCommMonoid.proof_3

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

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

instance UInt32.instPowNat_mathlib : Pow UInt32 ℕ

Equations

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

instance USize.neZero : NeZero USize.size

Equations

• USize.neZero = ⋯

instance UInt32.instSMulInt : SMul ℤ UInt32

Equations

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

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

def UInt8.instCommRing : CommRing UInt8

To use this instance, use open scoped UInt8.CommRing.

See the module docstring for an explanation

Equations

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

theorem UInt8.val_injective : Function.Injective UInt8.val

instance UInt8.instPowNat_mathlib : Pow UInt8 ℕ

Equations

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

def UInt16.instIntCast : IntCast UInt16

To use this instance, use open scoped UInt16.CommRing.

See the module docstring for an explanation

Equations

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

instance USize.instCommMonoid : CommMonoid USize

Equations

• USize.instCommMonoid = Function.Injective.commMonoid USize.val USize.val_injective USize.instCommMonoid.proof_1 USize.instCommMonoid.proof_2 USize.instCommMonoid.proof_3

theorem UInt32.val_injective : Function.Injective UInt32.val

instance UInt8.instNeg_mathlib : Neg UInt8

Equations

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

instance UInt8.instSMulNat : SMul ℕ UInt8

Equations

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

instance UInt8.instSMulInt : SMul ℤ UInt8

Equations

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

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

def UInt64.instNatCast : NatCast UInt64

To use this instance, use open scoped UInt64.CommRing.

See the module docstring for an explanation

Equations

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

def UInt16.instCommRing : CommRing UInt16

To use this instance, use open scoped UInt16.CommRing.

See the module docstring for an explanation

Equations

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

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

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

def USize.instIntCast : IntCast USize

To use this instance, use open scoped USize.CommRing.

See the module docstring for an explanation

Equations

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

instance USize.instNeg_mathlib : Neg USize

Equations

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

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

instance UInt64.instSMulInt : SMul ℤ UInt64

Equations

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

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

def USize.instNatCast : NatCast USize

To use this instance, use open scoped USize.CommRing.

See the module docstring for an explanation

Equations

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

instance USize.instSMulNat : SMul ℕ USize

Equations

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

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

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

instance UInt16.neZero : NeZero UInt16.size

Equations

• UInt16.neZero = ⋯

instance UInt8.neZero : NeZero UInt8.size

Equations

• UInt8.neZero = ⋯

def UInt8.isASCIIUpper (c : UInt8) : Bool

Is this an uppercase ASCII letter?

Equations

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

def UInt8.isASCIILower (c : UInt8) : Bool

Is this a lowercase ASCII letter?

Equations

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

def UInt8.isASCIIAlpha (c : UInt8) : Bool

Is this an alphabetic ASCII character?

Equations

• c.isASCIIAlpha = (c.isASCIIUpper || c.isASCIILower)

def UInt8.isASCIIDigit (c : UInt8) : Bool

Is this an ASCII digit character?

Equations

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

def UInt8.isASCIIAlphanum (c : UInt8) : Bool

Is this an alphanumeric ASCII character?

Equations

• c.isASCIIAlphanum = (c.isASCIIAlpha || c.isASCIIDigit)

@[deprecated UInt8.isASCIIUpper]

def UInt8.isUpper (c : UInt8) : Bool

Alias of UInt8.isASCIIUpper.

---

Is this an uppercase ASCII letter?

Equations

• UInt8.isUpper = UInt8.isASCIIUpper

@[deprecated UInt8.isASCIILower]

def UInt8.isLower (c : UInt8) : Bool

Alias of UInt8.isASCIILower.

---

Is this a lowercase ASCII letter?

Equations

• UInt8.isLower = UInt8.isASCIILower

@[deprecated UInt8.isASCIIAlpha]

def UInt8.isAlpha (c : UInt8) : Bool

Alias of UInt8.isASCIIAlpha.

---

Is this an alphabetic ASCII character?

Equations

• UInt8.isAlpha = UInt8.isASCIIAlpha

@[deprecated UInt8.isASCIIDigit]

def UInt8.isDigit (c : UInt8) : Bool

Alias of UInt8.isASCIIDigit.

---

Is this an ASCII digit character?

Equations

• UInt8.isDigit = UInt8.isASCIIDigit

@[deprecated UInt8.isASCIIAlphanum]

def UInt8.isAlphanum (c : UInt8) : Bool

Alias of UInt8.isASCIIAlphanum.

---

Is this an alphanumeric ASCII character?

Equations

• UInt8.isAlphanum = UInt8.isASCIIAlphanum

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

• n.toChar = { val := n.toUInt32, valid := ⋯ }