Mathlib.Data.UInt
source
Is this an uppercase ASCII letter?
Is this a lowercase ASCII letter?
Is this an alphabetic ASCII character?
Is this an ASCII digit character?
Is this an alphanumeric ASCII character?
The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.