@[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.

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

One character is less than another if its code point is strictly less than the other's.

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

One character is less than or equal to another if its code point is less than or equal to the other's.

instance Char.instLT : LT Char

instance Char.instLE : LE Char

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

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

@[reducible, inline]

abbrev Char.isValidCharNat (n : Nat) : Prop

True for natural numbers that are valid Unicode scalar values.

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

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

theorem Char.isValidChar_zero : isValidChar 0

@[inline]

def Char.toNat (c : Char) : Nat

The character's Unicode code point as a Nat.

@[inline]

def Char.toUInt8 (c : Char) : UInt8

Converts a character into a UInt8 that contains its code point.

If the code point is larger than 255, it is truncated (reduced modulo 256).

def Char.ofUInt8 (n : UInt8) : Char

Converts an 8-bit unsigned integer into a character.

The integer's value is interpreted as a Unicode code point.

instance Char.instInhabited : Inhabited Char

@[inline]

def Char.isWhitespace (c : Char) : Bool

Returns true if the character is a space (' ', U+0020), a tab ('\t', U+0009), a carriage return ('\r', U+000D), or a newline ('\n', U+000A).

@[inline]

def Char.isUpper (c : Char) : Bool

Returns true if the character is a uppercase ASCII letter.

The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

@[inline]

def Char.isLower (c : Char) : Bool

Returns true if the character is a lowercase ASCII letter.

The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.

@[inline]

def Char.isAlpha (c : Char) : Bool

Returns true if the character is an ASCII letter.

The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz.

@[inline]

def Char.isDigit (c : Char) : Bool

Returns true if the character is an ASCII digit.

The ASCII digits are the following: 0123456789.

@[inline]

def Char.isAlphanum (c : Char) : Bool

Returns true if the character is an ASCII letter or digit.

The ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz. The ASCII digits are the following: 0123456789.

def Char.toLower (c : Char) : Char

Converts an uppercase ASCII letter to the corresponding lowercase letter. Letters outside the ASCII alphabet are returned unchanged.

The uppercase ASCII letters are the following: ABCDEFGHIJKLMNOPQRSTUVWXYZ.

def Char.toUpper (c : Char) : Char

Converts a lowercase ASCII letter to the corresponding uppercase letter. Letters outside the ASCII alphabet are returned unchanged.

The lowercase ASCII letters are the following: abcdefghijklmnopqrstuvwxyz.