@[inline]

def Data.Word8.isUpper (w : UInt8) : Bool

Test if byte is an uppercase ASCII letter. $$\text{isUpper}(w) \iff w \in [65, 90]$$

Equations

• Data.Word8.isUpper w = (decide (65 ≤ w) && decide (w ≤ 90))

@[inline]

def Data.Word8.isLower (w : UInt8) : Bool

Test if byte is a lowercase ASCII letter. $$\text{isLower}(w) \iff w \in [97, 122]$$

Equations

• Data.Word8.isLower w = (decide (97 ≤ w) && decide (w ≤ 122))

@[inline]

def Data.Word8.isAlpha (w : UInt8) : Bool

Test if byte is an ASCII letter. $$\text{isAlpha}(w) \iff \text{isUpper}(w) \lor \text{isLower}(w)$$

Equations

• Data.Word8.isAlpha w = (Data.Word8.isUpper w || Data.Word8.isLower w)

@[inline]

def Data.Word8.isDigit (w : UInt8) : Bool

Test if byte is an ASCII decimal digit. $$\text{isDigit}(w) \iff w \in [48, 57]$$

Equations

• Data.Word8.isDigit w = (decide (48 ≤ w) && decide (w ≤ 57))

@[inline]

def Data.Word8.isAlphaNum (w : UInt8) : Bool

Test if byte is an ASCII letter or digit. $$\text{isAlphaNum}(w) \iff \text{isAlpha}(w) \lor \text{isDigit}(w)$$

Equations

• Data.Word8.isAlphaNum w = (Data.Word8.isAlpha w || Data.Word8.isDigit w)

@[inline]

def Data.Word8.isSpace (w : UInt8) : Bool

Test if byte is ASCII whitespace (space, tab, newline, vertical tab, form feed, carriage return). $$\text{isSpace}(w) \iff w \in \{9,10,11,12,13,32\}$$

Equations

• Data.Word8.isSpace w = (w == 32 || decide (9 ≤ w) && decide (w ≤ 13))

@[inline]

def Data.Word8.isControl (w : UInt8) : Bool

Test if byte is an ASCII control character. $$\text{isControl}(w) \iff w < 32 \lor w = 127$$

Equations

• Data.Word8.isControl w = (decide (w < 32) || w == 127)

@[inline]

def Data.Word8.isPrint (w : UInt8) : Bool

Test if byte is a printable ASCII character. $$\text{isPrint}(w) \iff w \in [32, 126]$$

Equations

• Data.Word8.isPrint w = (decide (32 ≤ w) && decide (w ≤ 126))

@[inline]

def Data.Word8.isHexDigit (w : UInt8) : Bool

Test if byte is an ASCII hexadecimal digit. $$\text{isHexDigit}(w) \iff \text{isDigit}(w) \lor w \in [65,70] \lor w \in [97,102]$$

Equations

• Data.Word8.isHexDigit w = (Data.Word8.isDigit w || decide (65 ≤ w) && decide (w ≤ 70) || decide (97 ≤ w) && decide (w ≤ 102))

@[inline]

def Data.Word8.isOctDigit (w : UInt8) : Bool

Test if byte is an ASCII octal digit. $$\text{isOctDigit}(w) \iff w \in [48, 55]$$

Equations

• Data.Word8.isOctDigit w = (decide (48 ≤ w) && decide (w ≤ 55))

@[inline]

def Data.Word8.isAscii (w : UInt8) : Bool

Test if byte is in the ASCII range. $$\text{isAscii}(w) \iff w \le 127$$

Equations

• Data.Word8.isAscii w = decide (w ≤ 127)

@[inline]

def Data.Word8.toLower (w : UInt8) : UInt8

Convert an uppercase ASCII letter to lowercase; other bytes unchanged. $$\text{toLower}(w) = \begin{cases} w + 32 & \text{if } w \in [65,90] \\ w & \text{otherwise} \end{cases}$$

Equations

• Data.Word8.toLower w = if Data.Word8.isUpper w = true then w + 32 else w

@[inline]

def Data.Word8.toUpper (w : UInt8) : UInt8

Convert a lowercase ASCII letter to uppercase; other bytes unchanged. $$\text{toUpper}(w) = \begin{cases} w - 32 & \text{if } w \in [97,122] \\ w & \text{otherwise} \end{cases}$$

Equations

• Data.Word8.toUpper w = if Data.Word8.isLower w = true then w - 32 else w

theorem Data.Word8.toLower_idempotent (w : UInt8) : toLower (toLower w) = toLower w

toLower is idempotent: applying it twice yields the same result. $$\forall w.\; \text{toLower}(\text{toLower}(w)) = \text{toLower}(w)$$

Proved by exhaustive evaluation over all 256 UInt8 values via native_decide.

theorem Data.Word8.toUpper_idempotent (w : UInt8) : toUpper (toUpper w) = toUpper w

toUpper is idempotent: applying it twice yields the same result. $$\forall w.\; \text{toUpper}(\text{toUpper}(w)) = \text{toUpper}(w)$$

Proved by exhaustive evaluation over all 256 UInt8 values via native_decide.

theorem Data.Word8.isUpper_toLower (w : UInt8) : isUpper w = true → isLower (toLower w) = true

toLower maps uppercase letters to lowercase letters. $$\forall w.\; \text{isUpper}(w) \to \text{isLower}(\text{toLower}(w))$$

Proved by exhaustive evaluation over all 256 UInt8 values via native_decide.

theorem Data.Word8.isLower_toUpper (w : UInt8) : isLower w = true → isUpper (toUpper w) = true

toUpper maps lowercase letters to uppercase letters. $$\forall w.\; \text{isLower}(w) \to \text{isUpper}(\text{toUpper}(w))$$

Proved by exhaustive evaluation over all 256 UInt8 values via native_decide.