@[inline, reducible]

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 : Char) (b : Char) : Prop

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

instance Char.instLTChar : LT Char

instance Char.instLEChar : LE Char

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

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

@[inline, reducible]

abbrev Char.isValidCharNat (n : Nat) : Prop

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

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

theorem Char.isValidChar_of_isValidChar_Nat (n : Nat) (h : Char.isValidCharNat n) : isValidChar (UInt32.ofNat' n (_ : n < UInt32.size))

theorem Char.isValidChar_zero : isValidChar 0

@[inline]

def Char.toNat (c : Char) : Nat

Underlying unicode code point as a Nat.

instance Char.instInhabitedChar : Inhabited Char

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)?

def Char.isUpper (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZ?

def Char.isLower (c : Char) : Bool

Is the character in abcdefghijklmnopqrstuvwxyz?

def Char.isAlpha (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz?

def Char.isDigit (c : Char) : Bool

Is the character in 0123456789?

def Char.isAlphanum (c : Char) : Bool

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789?

def Char.toLower (c : Char) : Char

Convert an upper case character to its lower case character.

Only works on basic latin letters.

def Char.toUpper (c : Char) : Char

Convert a lower case character to its upper case character.

Only works on basic latin letters.