@[reducible, inline]

def isValidChar (n : UInt32) : Prop

Determines if the given integer is a valid Unicode scalar value.

Note that values in [0xd800, 0xdfff] are reserved for UTF-16 surrogate pairs.

Equations

• isValidChar n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

def Char.lt (a : Char) (b : Char) : Prop

Equations

• a.lt b = (a.val < b.val)

def Char.le (a : Char) (b : Char) : Prop

Equations

• a.le b = (a.val ≤ b.val)

instance Char.instLT : LT Char

Equations

• Char.instLT = { lt := Char.lt }

instance Char.instLE : LE Char

Equations

• Char.instLE = { le := Char.le }

instance Char.instDecidableLt (a : Char) (b : Char) : Decidable (a < b)

Equations

• a.instDecidableLt b = a.val.decLt b.val

instance Char.instDecidableLe (a : Char) (b : Char) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = a.val.decLe b.val

@[reducible, inline]

abbrev Char.isValidCharNat (n : Nat) : Prop

Determines if the given nat is a valid Unicode scalar value.

Equations

• Char.isValidCharNat n = (n < 55296 ∨ 57343 < n ∧ n < 1114112)

theorem Char.isValidUInt32 (n : Nat) (h : Char.isValidCharNat n) : n < UInt32.size

theorem Char.isValidChar_of_isValidCharNat (n : Nat) (h : Char.isValidCharNat n) : isValidChar (UInt32.ofNat' n ⋯)

theorem Char.isValidChar_zero : isValidChar 0

@[inline]

def Char.toNat (c : Char) : Nat

Underlying unicode code point as a Nat.

Equations

• c.toNat = c.val.toNat

@[inline]

def Char.toUInt8 (c : Char) : UInt8

Convert a character into a UInt8, by truncating (reducing modulo 256) if necessary.

Equations

• c.toUInt8 = c.val.toUInt8

def Char.ofUInt8 (n : UInt8) : Char

The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other.

Equations

• Char.ofUInt8 n = { val := n.toUInt32, valid := ⋯ }

instance Char.instInhabited : Inhabited Char

Equations

• Char.instInhabited = { default := 'A' }

def Char.isWhitespace (c : Char) : Bool

Is the character a space (U+0020) a tab (U+0009), a carriage return (U+000D) or a newline (U+000A)?

Equations

• c.isWhitespace = (decide (c = ' ') || decide (c = '\t') || decide (c = '\x0d') || decide (c = '\n'))

def Char.isUpper (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZ?

Equations

• c.isUpper = (decide (c.val ≥ 65) && decide (c.val ≤ 90))

def Char.isLower (c : Char) : Bool

Is the character in abcdefghijklmnopqrstuvwxyz?

Equations

• c.isLower = (decide (c.val ≥ 97) && decide (c.val ≤ 122))

def Char.isAlpha (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz?

Equations

• c.isAlpha = (c.isUpper || c.isLower)

def Char.isDigit (c : Char) : Bool

Is the character in 0123456789?

Equations

• c.isDigit = (decide (c.val ≥ 48) && decide (c.val ≤ 57))

def Char.isAlphanum (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789?

Equations

• c.isAlphanum = (c.isAlpha || c.isDigit)

def Char.toLower (c : Char) : Char

Convert an upper case character to its lower case character.

Only works on basic latin letters.

Equations

• c.toLower = let n := c.toNat; if n ≥ 65 ∧ n ≤ 90 then Char.ofNat (n + 32) else c

def Char.toUpper (c : Char) : Char

Convert a lower case character to its upper case character.

Only works on basic latin letters.

Equations

• c.toUpper = let n := c.toNat; if n ≥ 97 ∧ n ≤ 122 then Char.ofNat (n - 32) else c