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.

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)

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 := ⋯ }