Documentation

Init.Data.Char.Basic

@[reducible, inline]

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
def Char.lt (a b : Char) :
Equations
  • a.lt b = (a.val < b.val)
def Char.le (a b : Char) :
Equations
  • a.le b = (a.val b.val)
instance Char.instLT :
Equations
instance Char.instLE :
Equations
instance Char.instDecidableLt (a b : Char) :
Decidable (a < b)
Equations
  • a.instDecidableLt b = a.val.decLt b.val
instance Char.instDecidableLe (a b : Char) :
Equations
  • a.instDecidableLe b = a.val.decLe b.val
@[reducible, inline]

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

Equations
@[inline]
def Char.toNat (c : Char) :

Underlying unicode code point as a Nat.

Equations
  • c.toNat = c.val.toNat
@[inline]

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

Equations
  • c.toUInt8 = c.val.toUInt8

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

Equations
Equations
@[inline]

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

Equations
@[inline]

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZ?

Equations
@[inline]

Is the character in abcdefghijklmnopqrstuvwxyz?

Equations
@[inline]

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz?

Equations
  • c.isAlpha = (c.isUpper || c.isLower)
@[inline]

Is the character in 0123456789?

Equations
@[inline]

Is the character in ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789?

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

Convert an upper case character to its lower case character.

Only works on basic latin letters.

Equations

Convert a lower case character to its upper case character.

Only works on basic latin letters.

Equations