source
@[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)

Instances For

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

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

Equations

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

Instances For

source
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.

Equations

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

Instances For

source
instance Char.instLT :
LT Char
Equations

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

source
instance Char.instLE :
LE Char
Equations

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

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

- a.instDecidableLt b = a.val.decLt b.val

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

- a.instDecidableLe b = a.val.decLe b.val

source
@[reducible, inline]
abbrev Char.isValidCharNat (n : Nat) :
Prop

True for natural numbers that are valid Unicode scalar values.

Equations

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

Instances For

source
theorem Char.isValidUInt32 (n : Nat) (h : isValidCharNat n) :
n < UInt32.size
source
theorem Char.isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) :
isValidChar (UInt32.ofNatLT n ⋯)
source
theorem Char.isValidChar_zero :
isValidChar 0
source
@[inline]
def Char.toNat (c : Char) :
Nat

The character's Unicode code point as a `Nat`.

Equations

- c.toNat = c.val.toNat

Instances For

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

Equations

- c.toUInt8 = c.val.toUInt8

Instances For

source
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.

Equations

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

Instances For

source
instance Char.instInhabited :
Inhabited Char
Equations

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

source
@[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)`.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

source
@[inline]
def Char.isAlpha (c : Char) :
Bool

Returns `true` if the character is an ASCII letter.

The ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`.

Equations

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

Instances For

source
@[inline]
def Char.isDigit (c : Char) :
Bool

Returns `true` if the character is an ASCII digit.

The ASCII digits are the following: `0123456789`.

Equations

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

Instances For

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

Equations

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

Instances For

source
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`.

Equations

- c.toLower = if c.toNat ≥ 65 ∧ c.toNat ≤ 90 then Char.ofNat (c.toNat + 32) else c

Instances For

source
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`.

Equations

- c.toUpper = if c.toNat ≥ 97 ∧ c.toNat ≤ 122 then Char.ofNat (c.toNat - 32) else c

Instances For