@[inline]

def Data.Char'.isSpace (c : Char) : Bool

Alias for Char.isWhitespace. $$\text{isSpace}(c) = \text{isWhitespace}(c)$$

Equations

• Data.Char'.isSpace c = c.isWhitespace

@[inline]

def Data.Char'.isAlphaNum (c : Char) : Bool

Test if a character is alphanumeric (letter or digit). $$\text{isAlphaNum}(c) = \text{isAlpha}(c) \lor \text{isDigit}(c)$$

Equations

• Data.Char'.isAlphaNum c = (c.isAlpha || c.isDigit)

@[inline]

def Data.Char'.isAscii (c : Char) : Bool

Test if a character is in the ASCII range $[0, 128)$. $$\text{isAscii}(c) \iff \text{ord}(c) < 128$$

Equations

• Data.Char'.isAscii c = decide (c.toNat < 128)

@[inline]

def Data.Char'.isLatin1 (c : Char) : Bool

Test if a character is in the Latin-1 range $[0, 256)$. $$\text{isLatin1}(c) \iff \text{ord}(c) < 256$$

Equations

• Data.Char'.isLatin1 c = decide (c.toNat < 256)

@[inline]

def Data.Char'.isControl (c : Char) : Bool

Test if a character is a control character (codes 0--31 or 127). $$\text{isControl}(c) \iff \text{ord}(c) < 32 \lor \text{ord}(c) = 127$$

Equations

• Data.Char'.isControl c = (decide (c.toNat < 32) || c.toNat == 127)

@[inline]

def Data.Char'.isPrint (c : Char) : Bool

Test if a character is printable (ASCII, non-control). $$\text{isPrint}(c) \iff \lnot\,\text{isControl}(c) \land \text{ord}(c) < 128$$ Note: this is a simplified ASCII-only version.

Equations

• Data.Char'.isPrint c = (!Data.Char'.isControl c && decide (c.toNat < 128))

@[inline]

def Data.Char'.isHexDigit (c : Char) : Bool

Test if a character is a hexadecimal digit: 0--9, a--f, A--F. $$\text{isHexDigit}(c) \iff c \in [0\text{-}9] \cup [a\text{-}f] \cup [A\text{-}F]$$

Equations

• Data.Char'.isHexDigit c = (c.isDigit || decide (c.toNat ≥ 65) && decide (c.toNat ≤ 70) || decide (c.toNat ≥ 97) && decide (c.toNat ≤ 102))

@[inline]

def Data.Char'.isOctDigit (c : Char) : Bool

Test if a character is an octal digit: 0--7. $$\text{isOctDigit}(c) \iff \text{ord}(c) \in [48, 55]$$

Equations

• Data.Char'.isOctDigit c = (decide (c.toNat ≥ 48) && decide (c.toNat ≤ 55))

@[inline]

def Data.Char'.isAsciiUpper (c : Char) : Bool

Test if a character is an ASCII uppercase letter: A--Z. $$\text{isAsciiUpper}(c) \iff \text{ord}(c) \in [65, 90]$$

Equations

• Data.Char'.isAsciiUpper c = (decide (c.toNat ≥ 65) && decide (c.toNat ≤ 90))

@[inline]

def Data.Char'.isAsciiLower (c : Char) : Bool

Test if a character is an ASCII lowercase letter: a--z. $$\text{isAsciiLower}(c) \iff \text{ord}(c) \in [97, 122]$$

Equations

• Data.Char'.isAsciiLower c = (decide (c.toNat ≥ 97) && decide (c.toNat ≤ 122))

@[inline]

def Data.Char'.isPunctuation (c : Char) : Bool

Test if a character is ASCII punctuation. $$\text{isPunctuation}(c) \iff c \in [\texttt{!}-\texttt{/}] \cup [\texttt{:}-\texttt{@}] \cup [\texttt{[}-\texttt{`}] \cup [\texttt{\{}-\texttt{~}]$$ Covers ASCII punctuation ranges: 33--47, 58--64, 91--96, 123--126.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Data.Char'.ord (c : Char) : Nat

Character to its Unicode code point. $$\text{ord}(c) = \text{toNat}(c)$$

Equations

• Data.Char'.ord c = c.toNat

@[inline]

def Data.Char'.chr (n : Nat) : Char

Code point to character. $$\text{chr}(n) = \text{Char.ofNat}(n)$$

Equations

• Data.Char'.chr n = Char.ofNat n

def Data.Char'.digitToInt (c : Char) : Option { n : Nat // n < 16 }

Convert a hex digit character to its numeric value, bounded below 16. $$\text{digitToInt}(c) = \begin{cases} n - 48 & c \in [\texttt{0}\text{-}\texttt{9}] \\ n - 55 & c \in [\texttt{A}\text{-}\texttt{F}] \\ n - 87 & c \in [\texttt{a}\text{-}\texttt{f}] \\ \text{none} & \text{otherwise} \end{cases}$$ Returns Option {n : Nat // n < 16} — the proof that the digit is in $[0, 15]$ is carried in the subtype and erased at runtime.

Equations

• One or more equations did not get rendered due to their size.

def Data.Char'.intToDigit (n : Nat) (_h : n < 16 := by omega) : Char

Convert a number in $[0, 15]$ to a hex digit character. Total — no Option needed. $$\text{intToDigit}(n) = \begin{cases} \texttt{0} + n & n \in [0, 9] \\ \texttt{a} + (n - 10) & n \in [10, 15] \end{cases}$$ The proof obligation n < 16 is required at the call site and erased at runtime.

Equations

• Data.Char'.intToDigit n _h = if n ≤ 9 then Char.ofNat (48 + n) else Char.ofNat (87 + n)

theorem Data.Char'.isAlphaNum_iff (c : Char) : isAlphaNum c = (c.isAlpha || c.isDigit)

isAlphaNum unfolds to its definition.

theorem Data.Char'.isSpace_eq_isWhitespace (c : Char) : isSpace c = c.isWhitespace

isSpace is an alias for isWhitespace.

theorem Data.Char'.ord_eq_toNat (c : Char) : ord c = c.toNat

ord is an alias for toNat.

theorem Data.Char'.isAscii_bound (c : Char) (h : isAscii c = true) : c.toNat < 128

isAscii c = true implies c.toNat < 128.

theorem Data.Char'.digitToInt_intToDigit (n : Nat) (h : n < 16) : digitToInt (intToDigit n h) = some ⟨n, h⟩

Roundtrip: digitToInt (intToDigit n) = some ⟨n, h⟩ for all n < 16.

theorem Data.Char'.isAscii_iff (c : Char) : isAscii c = true ↔ c.toNat < 128

isAscii is true iff the code point is below 128.

theorem Data.Char'.isHexDigit_of_digit (c : Char) (h : c.isDigit = true) : isHexDigit c = true

Every decimal digit is also a hex digit.

theorem Data.Char'.intToDigit_isAscii (n : Nat) (h : n < 16) : isAscii (intToDigit n h) = true

intToDigit always produces an ASCII character.