Documentation

Mathlib.Data.UInt

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.

@[simp]

theorem UInt8.toBitVec_zsmul (z : ℤ) (a : UInt8) :

(z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt64.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

theorem UInt64.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_zsmul (z : ℤ) (a : USize) :

(z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt32.toBitVec_zsmul (z : ℤ) (a : UInt32) :

(z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt64.toBitVec_zsmul (z : ℤ) (a : UInt64) :

(z • a).toBitVec = z • a.toBitVec

@[simp]

theorem UInt32.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

theorem UInt32.toBitVec_nsmul (n : ℕ) (a : UInt32) :

(n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt16.toBitVec_zsmul (z : ℤ) (a : UInt16) :

(z • a).toBitVec = z • a.toBitVec

theorem UInt64.toBitVec_nsmul (n : ℕ) (a : UInt64) :

(n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt32.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

theorem UInt16.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

theorem USize.toBitVec_nsmul (n : ℕ) (a : USize) :

(n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt16.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

theorem UInt8.toBitVec_nsmul (n : ℕ) (a : UInt8) :

(n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt32.toBitVec_pow (a : UInt32) (n : ℕ) :

(a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt8.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

theorem UInt64.toBitVec_pow (a : UInt64) (n : ℕ) :

(a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem UInt8.toBitVec_pow (a : UInt8) (n : ℕ) :

(a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem USize.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

theorem UInt16.toBitVec_nsmul (n : ℕ) (a : UInt16) :

(n • a).toBitVec = n • a.toBitVec

@[simp]

theorem UInt8.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

theorem UInt16.toBitVec_pow (a : UInt16) (n : ℕ) :

(a ^ n).toBitVec = a.toBitVec ^ n

@[simp]

theorem USize.toBitVec_pow (a : USize) (n : ℕ) :

(a ^ n).toBitVec = a.toBitVec ^ n

instance UInt32.instNonUnitalCommRing :

NonUnitalCommRing UInt32

Equations

instance UInt64.instNonUnitalCommRing :

NonUnitalCommRing UInt64

Equations

instance UInt64.instCommMonoid :

CommMonoid UInt64

Equations

theorem UInt64.toBitVec_injective :

Function.Injective toBitVec

theorem USize.toBitVec_injective :

Function.Injective toBitVec

instance UInt32.instCommMonoid :

CommMonoid UInt32

Equations

def UInt32.instCommRing :

CommRing UInt32

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

See the module docstring for an explanation

Equations

Instances For

def UInt64.instCommRing :

CommRing UInt64

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

See the module docstring for an explanation

Equations

Instances For

instance UInt16.instNonUnitalCommRing :

NonUnitalCommRing UInt16

Equations

def UInt8.instCommRing :

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

See the module docstring for an explanation

Equations

Instances For

def UInt16.instCommRing :

CommRing UInt16

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

See the module docstring for an explanation

Equations

Instances For

theorem UInt32.toBitVec_injective :

Function.Injective toBitVec

theorem UInt16.toBitVec_injective :

Function.Injective toBitVec

theorem UInt32.toFin_injective :

Function.Injective toFin

instance USize.instCommMonoid :

CommMonoid USize

Equations

instance UInt8.instCommMonoid :

CommMonoid UInt8

Equations

theorem UInt16.toFin_injective :

Function.Injective toFin

theorem USize.toFin_injective :

Function.Injective toFin

theorem UInt8.toBitVec_injective :

Function.Injective toBitVec

def USize.instCommRing :

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

See the module docstring for an explanation

Equations

Instances For

instance UInt8.instNonUnitalCommRing :

NonUnitalCommRing UInt8

Equations

instance USize.instNonUnitalCommRing :

NonUnitalCommRing USize

Equations

theorem UInt8.toFin_injective :

Function.Injective toFin

instance UInt16.instCommMonoid :

CommMonoid UInt16

Equations

theorem UInt64.toFin_injective :

Function.Injective toFin

def UInt8.isASCIIUpper (c : UInt8) :

Is this an uppercase ASCII letter?

Equations

Instances For

def UInt8.isASCIILower (c : UInt8) :

Is this a lowercase ASCII letter?

Equations

Instances For

def UInt8.isASCIIAlpha (c : UInt8) :

Is this an alphabetic ASCII character?

Equations

Instances For

def UInt8.isASCIIDigit (c : UInt8) :

Is this an ASCII digit character?

Equations

Instances For

def UInt8.isASCIIAlphanum (c : UInt8) :

Is this an alphanumeric ASCII character?

Equations

Instances For

def UInt8.toChar (n : UInt8) :

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

Equations

Instances For