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 USize.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

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

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

@[simp]

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

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

@[simp]

theorem UInt32.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

theorem USize.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

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

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

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

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

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

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

@[simp]

theorem UInt8.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[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 UInt16.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

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

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

@[simp]

theorem UInt32.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

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

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

@[simp]

theorem UInt64.toBitVec_natCast (n : ℕ) :

(↑n).toBitVec = ↑n

@[simp]

theorem UInt8.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

theorem UInt64.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

@[simp]

theorem UInt16.toBitVec_intCast (z : ℤ) :

(↑z).toBitVec = ↑z

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

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

@[implicit_reducible]

instance UInt32.instNonUnitalCommRing :

NonUnitalCommRing UInt32

theorem UInt8.toBitVec_injective :

Function.Injective toBitVec

@[implicit_reducible]

noncomputable def UInt16.instCommRing :

CommRing UInt16

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

See the module docstring for an explanation

Instances For

@[implicit_reducible]

noncomputable def USize.instCommRing :

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

See the module docstring for an explanation

Instances For

@[implicit_reducible]

noncomputable def UInt32.instCommRing :

CommRing UInt32

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

See the module docstring for an explanation

Instances For

theorem UInt64.toFin_injective :

Function.Injective toFin

@[implicit_reducible]

instance UInt64.instNonUnitalCommRing :

NonUnitalCommRing UInt64

theorem USize.toBitVec_injective :

Function.Injective toBitVec

@[implicit_reducible]

noncomputable def UInt64.instCommRing :

CommRing UInt64

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

See the module docstring for an explanation

Instances For

@[implicit_reducible]

instance UInt32.instCommMonoid :

CommMonoid UInt32

@[implicit_reducible]

instance UInt8.instCommMonoid :

CommMonoid UInt8

theorem UInt16.toBitVec_injective :

Function.Injective toBitVec

theorem UInt32.toBitVec_injective :

Function.Injective toBitVec

theorem USize.toFin_injective :

Function.Injective toFin

@[implicit_reducible]

instance UInt8.instNonUnitalCommRing :

NonUnitalCommRing UInt8

theorem UInt8.toFin_injective :

Function.Injective toFin

theorem UInt64.toBitVec_injective :

Function.Injective toBitVec

@[implicit_reducible]

noncomputable def UInt8.instCommRing :

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

See the module docstring for an explanation

Instances For

@[implicit_reducible]

instance UInt16.instNonUnitalCommRing :

NonUnitalCommRing UInt16

@[implicit_reducible]

instance UInt64.instCommMonoid :

CommMonoid UInt64

@[implicit_reducible]

instance USize.instNonUnitalCommRing :

NonUnitalCommRing USize

@[implicit_reducible]

instance UInt16.instCommMonoid :

CommMonoid UInt16

theorem UInt32.toFin_injective :

Function.Injective toFin

theorem UInt16.toFin_injective :

Function.Injective toFin

@[implicit_reducible]

instance USize.instCommMonoid :

CommMonoid USize

def UInt8.isASCIIUpper (c : UInt8) :

Bool

Is this an uppercase ASCII letter?

Instances For

def UInt8.isASCIILower (c : UInt8) :

Bool

Is this a lowercase ASCII letter?

Instances For

def UInt8.isASCIIAlpha (c : UInt8) :

Bool

Is this an alphabetic ASCII character?

Instances For

def UInt8.isASCIIDigit (c : UInt8) :

Bool

Is this an ASCII digit character?

Instances For

def UInt8.isASCIIAlphanum (c : UInt8) :

Bool

Is this an alphanumeric ASCII character?

Instances For

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.

Instances For