General API

As a general rule, for a given a Unicode property called Unicode_Property, for example:

• If the property is boolean valued then the implementation is called Unicode.isUnicodeProperty.

• Otherwise, the implementation is called Unicode.getUnicodeProperty.

• If the value is not of standard type (Bool, Char, Nat, Int, etc.) or a combination thereof (e.g. Bool × Option Nat) then the value type is defined in UnicodeBasic.Types.

• If the input type needs disambiguation (e.g. Char vs String) the type name may be appended to the name as in Unicode.isUnicodePropertyChar or in Unicode.getUnicodePropertyString.

• If the output type is Option _ then the suffix ? may be appended to indicate that this is a partial function. In this case, a companion function with the suffix ! may be implemented. This function will perform the same calculation as the original but it assumes the user has checked that the input is in the domain, the function may panic if this is not the case.

There are exceptions and variations on these general rules. For example, Unicode.isInGeneralCategory checks whether a character belongs to a given general category. Because of derived general categories, this makes more sense than what the first rule above would give.

Some properties may be grouped in a namespace. The namespace Unicode.GeneralCategory is such. For example, Unicode.GeneralCategory.isL checks whether a character belongs to the derived general category L.

Name

@[inline]

def Unicode.getName (char : Char) : String

Get character name

When the Unicode property Name is empty, a unique code label is returned as described in Unicode Standard, section 4.8. These labels start with '<' (U+003C) and end with '>' (U+003E) so they are distinguishable from actual name values.

Unicode property: Name

Equations

• Unicode.getName char = (Unicode.getUnicodeData char).characterName.toString

Bidirectional Properties

@[inline]

def Unicode.getBidiClass (char : Char) : Unicode.BidiClass

Get character bidirectional class

Unicode property: Bidi_Class

Equations

• Unicode.getBidiClass char = (Unicode.getUnicodeData char).bidiClass

@[inline]

def Unicode.isBidiMirrored (char : Char) : Bool

Check if bidirectional mirrored character

Unicode property: Bidi_Mirrored

Equations

• Unicode.isBidiMirrored char = (Unicode.getUnicodeData char).bidiMirrored

@[inline]

def Unicode.isBidiControl (char : Char) : Bool

Check if bidirectional control character

Unicode property: Bidi_Control

Equations

• One or more equations did not get rendered due to their size.

General Category

@[inline]

def Unicode.getGeneralCategory (char : Char) : Unicode.GeneralCategory

Get character general category

Caveat: This function never returns a derived general category. Use Unicode.isInGeneralCategory to check whether a character belongs to a general category (derived or not).

Unicode property: General_Category

Equations

• Unicode.getGeneralCategory char = (Unicode.getUnicodeData char).generalCategory

@[inline]

def Unicode.isInGeneralCategory (char : Char) (category : Unicode.GeneralCategory) : Bool

Check if character belongs to the general category

Unicode property: General_Category

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.GeneralCategory.isLetter (char : Char) : Bool

Check if letter character (L)

This is a derived category (L = Lu | Ll | Lt | Lm | Lo).

Unicode Property: General_Category=L

Equations

• Unicode.GeneralCategory.isLetter char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.letter, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isL (char : Char) : Bool

Check if letter character (L)

This is a derived category (L = Lu | Ll | Lt | Lm | Lo).

Unicode Property: General_Category=L

Equations

• Unicode.GeneralCategory.isL = Unicode.GeneralCategory.isLetter

@[inline]

def Unicode.GeneralCategory.isLowercaseLetter (char : Char) : Bool

Check if lowercase letter character (Ll)

Unicode Property: General_Category=Ll

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLl (char : Char) : Bool

Check if lowercase letter character (Ll)

Unicode Property: General_Category=Ll

Equations

• Unicode.GeneralCategory.isLl = Unicode.GeneralCategory.isLowercaseLetter

@[inline]

def Unicode.GeneralCategory.isTitlecaseLetter (char : Char) : Bool

Check if titlecase letter character (Lt)

Unicode Property: General_Category=Lt

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLt (char : Char) : Bool

Check if titlecase letter character (Lt)

Unicode Property: General_Category=Lt

Equations

• Unicode.GeneralCategory.isLt = Unicode.GeneralCategory.isTitlecaseLetter

@[inline]

def Unicode.GeneralCategory.isUppercaseLetter (char : Char) : Bool

Check if uppercase letter character (Lu)

Unicode Property: General_Category=Lu

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLu (char : Char) : Bool

Check if uppercase letter character (Lu)

Unicode Property: General_Category=Lu

Equations

• Unicode.GeneralCategory.isLu = Unicode.GeneralCategory.isUppercaseLetter

@[inline]

def Unicode.GeneralCategory.isCasedLetter (char : Char) : Bool

Check if cased letter character (LC)

This is a derived category (L = Lu | Ll | Lt).

Unicode Property: General_Category=LC

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLC (char : Char) : Bool

Check if cased letter character (LC)

This is a derived category (L = Lu | Ll | Lt).

Unicode Property: General_Category=LC

Equations

• Unicode.GeneralCategory.isLC = Unicode.GeneralCategory.isCasedLetter

@[inline]

def Unicode.GeneralCategory.isModifierLetter (char : Char) : Bool

Check if modifier letter character (Lm)

Unicode Property: General_Category=Lm

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLm (char : Char) : Bool

Check if modifier letter character (Lm)

Unicode Property: General_Category=Lm

Equations

• Unicode.GeneralCategory.isLm = Unicode.GeneralCategory.isModifierLetter

@[inline]

def Unicode.GeneralCategory.isOtherLetter (char : Char) : Bool

Check if other letter character (Lo)

Unicode Property: General_Category=Lo

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isLo (char : Char) : Bool

Check if other letter character (Lo)

Unicode Property: General_Category=Lo

Equations

• Unicode.GeneralCategory.isLo = Unicode.GeneralCategory.isOtherLetter

@[inline]

def Unicode.GeneralCategory.isMark (char : Char) : Bool

Check if mark character (M)

This is a derived category (M = Mn | Mc | Me).

Unicode Property: General_Category=M

Equations

• Unicode.GeneralCategory.isMark char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.mark, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isM (char : Char) : Bool

Check if mark character (M)

This is a derived category (M = Mn | Mc | Me).

Unicode Property: General_Category=M

Equations

• Unicode.GeneralCategory.isM = Unicode.GeneralCategory.isMark

@[inline]

def Unicode.GeneralCategory.isNonspacingMark (char : Char) : Bool

Check if nonspacing combining mark character (Mn)

Unicode Property: General_Category=Mn

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isMn (char : Char) : Bool

Check if nonspacing combining mark character (Mn)

Unicode Property: General_Category=Mn

Equations

• Unicode.GeneralCategory.isMn = Unicode.GeneralCategory.isNonspacingMark

@[inline]

def Unicode.GeneralCategory.isSpacingMark (char : Char) : Bool

Check if spacing combining mark character (Mc)

Unicode Property: General_Category=Mc

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isMc (char : Char) : Bool

Check if spacing combining mark character (Mc)

Unicode Property: General_Category=Mc

Equations

• Unicode.GeneralCategory.isMc = Unicode.GeneralCategory.isSpacingMark

@[inline]

def Unicode.GeneralCategory.isEnclosingMark (char : Char) : Bool

Check if enclosing combining mark character (Me)

Unicode Property: General_Category=Me

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isMe (char : Char) : Bool

Check if enclosing combining mark character (Me)

Unicode Property: General_Category=Me

Equations

• Unicode.GeneralCategory.isMe = Unicode.GeneralCategory.isEnclosingMark

@[inline]

def Unicode.GeneralCategory.isNumber (char : Char) : Bool

Check if number character (N)

This is a derived category (N = Nd | Nl | No).

Unicode Property: General_Category=N

Equations

• Unicode.GeneralCategory.isNumber char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.number, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isN (char : Char) : Bool

Check if number character (N)

This is a derived category (N = Nd | Nl | No).

Unicode Property: General_Category=N

Equations

• Unicode.GeneralCategory.isN = Unicode.GeneralCategory.isNumber

@[inline]

def Unicode.GeneralCategory.isDecimalNumber (char : Char) : Bool

Check if decimal number character (Nd)

Unicode Property: General_Category=Nd

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isNd (char : Char) : Bool

Check if decimal number character (Nd)

Unicode Property: General_Category=Nd

Equations

• Unicode.GeneralCategory.isNd = Unicode.GeneralCategory.isDecimalNumber

@[inline]

def Unicode.GeneralCategory.isLetterNumber (char : Char) : Bool

Check if letter number character (Nl)

Unicode Property: General_Category=Nl

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isNl (char : Char) : Bool

Check if letter number character (Nl)

Unicode Property: General_Category=Nl

Equations

• Unicode.GeneralCategory.isNl = Unicode.GeneralCategory.isLetterNumber

@[inline]

def Unicode.GeneralCategory.isOtherNumber (char : Char) : Bool

Check if other number character (No)

Unicode Property: General_Category=No

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isNo (char : Char) : Bool

Check if other number character (No)

Unicode Property: General_Category=No

Equations

• Unicode.GeneralCategory.isNo = Unicode.GeneralCategory.isOtherNumber

@[inline]

def Unicode.GeneralCategory.isPunctuation (char : Char) : Bool

Check if punctuation character (P)

This is a derived category (P = Pc | Pd | Ps | Pe | Pi | Pf | Po).

Unicode Property: General_Category=P

Equations

• Unicode.GeneralCategory.isPunctuation char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.punctuation, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isP (char : Char) : Bool

Check if punctuation character (P)

This is a derived category (P = Pc | Pd | Ps | Pe | Pi | Pf | Po).

Unicode Property: General_Category=P

Equations

• Unicode.GeneralCategory.isP = Unicode.GeneralCategory.isPunctuation

@[inline]

def Unicode.GeneralCategory.isConnectorPunctuation (char : Char) : Bool

Check if connector punctuation character (Pc)

Unicode Property: General_Category=Pc

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPc (char : Char) : Bool

Check if connector punctuation character (Pc)

Unicode Property: General_Category=Pc

Equations

• Unicode.GeneralCategory.isPc = Unicode.GeneralCategory.isConnectorPunctuation

@[inline]

def Unicode.GeneralCategory.isDashPunctuation (char : Char) : Bool

Check if dash punctuation character (Pd)

Unicode Property: General_Category=Pd

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPd (char : Char) : Bool

Check if dash punctuation character (Pd)

Unicode Property: General_Category=Pd

Equations

• Unicode.GeneralCategory.isPd = Unicode.GeneralCategory.isDashPunctuation

@[inline]

def Unicode.GeneralCategory.isOpenPunctuation (char : Char) : Bool

Check if open punctuation character (Ps)

Unicode Property: General_Category=Ps

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPs (char : Char) : Bool

Check if open punctuation character (Ps)

Unicode Property: General_Category=Ps

Equations

• Unicode.GeneralCategory.isPs = Unicode.GeneralCategory.isOpenPunctuation

@[inline]

def Unicode.GeneralCategory.isClosePunctuation (char : Char) : Bool

Check if close punctuation character (Pe)

Unicode Property: General_Category=Pe

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPe (char : Char) : Bool

Check if close punctuation character (Pe)

Unicode Property: General_Category=Pe

Equations

• Unicode.GeneralCategory.isPe = Unicode.GeneralCategory.isClosePunctuation

@[inline]

def Unicode.GeneralCategory.isInitialPunctuation (char : Char) : Bool

Check if initial punctuation character (Pi)

Unicode Property: General_Category=Pi

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPi (char : Char) : Bool

Check if initial punctuation character (Pi)

Unicode Property: General_Category=Pi

Equations

• Unicode.GeneralCategory.isPi = Unicode.GeneralCategory.isInitialPunctuation

@[inline]

def Unicode.GeneralCategory.isFinalPunctuation (char : Char) : Bool

Check if initial punctuation character (Pf)

Unicode Property: General_Category=Pf

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPf (char : Char) : Bool

Check if initial punctuation character (Pf)

Unicode Property: General_Category=Pf

Equations

• Unicode.GeneralCategory.isPf = Unicode.GeneralCategory.isFinalPunctuation

@[inline]

def Unicode.GeneralCategory.isOtherPunctuation (char : Char) : Bool

Check if other punctuation character (Po)

Unicode Property: General_Category=Po

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isPo (char : Char) : Bool

Check if other punctuation character (Po)

Unicode Property: General_Category=Po

Equations

• Unicode.GeneralCategory.isPo = Unicode.GeneralCategory.isOtherPunctuation

@[inline]

def Unicode.GeneralCategory.isSymbol (char : Char) : Bool

Check if symbol character (S)

This is a derived category (S = Sm | Sc | Sk | So).

Unicode Property: General_Category=S

Equations

• Unicode.GeneralCategory.isSymbol char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.symbol, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isS (char : Char) : Bool

Check if symbol character (S)

This is a derived category (S = Sm | Sc | Sk | So).

Unicode Property: General_Category=S

Equations

• Unicode.GeneralCategory.isS = Unicode.GeneralCategory.isSymbol

@[inline]

def Unicode.GeneralCategory.isMathSymbol (char : Char) : Bool

Check if math symbol character (Sm)

Unicode Property: General_Category=Sm

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isSm (char : Char) : Bool

Check if math symbol character (Sm)

Unicode Property: General_Category=Sm

Equations

• Unicode.GeneralCategory.isSm = Unicode.GeneralCategory.isMathSymbol

def Unicode.GeneralCategory.isCurrencySymbol (char : Char) : Bool

Check if currency symbol character (Sc)

Unicode Property: General_Category=Sc

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isSc (char : Char) : Bool

Check if currency symbol character (Sc)

Unicode Property: General_Category=Sc

Equations

• Unicode.GeneralCategory.isSc = Unicode.GeneralCategory.isCurrencySymbol

@[inline]

def Unicode.GeneralCategory.isModifierSymbol (char : Char) : Bool

Check if modifier symbol character (Sk)

Unicode Property: General_Category=Sk

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isSk (char : Char) : Bool

Check if modifier symbol character (Sk)

Unicode Property: General_Category=Sk

Equations

• Unicode.GeneralCategory.isSk = Unicode.GeneralCategory.isModifierSymbol

@[inline]

def Unicode.GeneralCategory.isOtherSymbol (char : Char) : Bool

Check if other symbol character (So)

Unicode Property: General_Category=So

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isSo (char : Char) : Bool

Check if other symbol character (So)

Unicode Property: General_Category=So

Equations

• Unicode.GeneralCategory.isSo = Unicode.GeneralCategory.isOtherSymbol

@[inline]

def Unicode.GeneralCategory.isSeparator (char : Char) : Bool

Check if separator character (Z)

This is a derived property (Z = Zs | Zl | Zp).

Unicode Property: General_Category=Z

Equations

• Unicode.GeneralCategory.isSeparator char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.separator, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isZ (char : Char) : Bool

Check if separator character (Z)

This is a derived property (Z = Zs | Zl | Zp).

Unicode Property: General_Category=Z

Equations

• Unicode.GeneralCategory.isZ = Unicode.GeneralCategory.isSeparator

@[inline]

def Unicode.GeneralCategory.isSpaceSeparator (char : Char) : Bool

Check if space separator character (Zs)

Unicode Property: General_Category=Zs

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isZs (char : Char) : Bool

Check if space separator character (Zs)

Unicode Property: General_Category=Zs

Equations

• Unicode.GeneralCategory.isZs = Unicode.GeneralCategory.isSpaceSeparator

@[inline]

def Unicode.GeneralCategory.isLineSeparator (char : Char) : Bool

Check if line separator character (Zl)

Unicode Property: General_Category=Zl

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isZl (char : Char) : Bool

Check if line separator character (Zl)

Unicode Property: General_Category=Zl

Equations

• Unicode.GeneralCategory.isZl = Unicode.GeneralCategory.isLineSeparator

@[inline]

def Unicode.GeneralCategory.isParagraphSeparator (char : Char) : Bool

Check if paragraph separator character (Zp)

Unicode Property: General_Category=Zp

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isZp (char : Char) : Bool

Check if paragraph separator character (Zp)

Unicode Property: General_Category=Zp

Equations

• Unicode.GeneralCategory.isZp = Unicode.GeneralCategory.isParagraphSeparator

@[inline]

def Unicode.GeneralCategory.isOther (char : Char) : Bool

Check if other character (C)

This is a derived category (C = Cc | Cf | Cs | Co | Cn).

Unicode Property: General_Category=C

Equations

• Unicode.GeneralCategory.isOther char = match Unicode.getGeneralCategory char with | { major := Unicode.MajorGeneralCategory.other, minor := minor } => true | x => false

@[reducible, inline]

abbrev Unicode.GeneralCategory.isC (char : Char) : Bool

Check if other character (C)

This is a derived category (C = Cc | Cf | Cs | Co | Cn).

Unicode Property: General_Category=C

Equations

• Unicode.GeneralCategory.isC = Unicode.GeneralCategory.isOther

@[inline]

def Unicode.GeneralCategory.isControl (char : Char) : Bool

Check if control character (Cc)

Unicode Property: General_Category=Cc

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isCc (char : Char) : Bool

Check if control character (Cc)

Unicode Property: General_Category=Cc

Equations

• Unicode.GeneralCategory.isCc = Unicode.GeneralCategory.isControl

@[inline]

def Unicode.GeneralCategory.isFormat (char : Char) : Bool

Check if format character (Cf)

Unicode Property: General_Category=Cf

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isCf (char : Char) : Bool

Check if format character (Cf)

Unicode Property: General_Category=Cf

Equations

• Unicode.GeneralCategory.isCf = Unicode.GeneralCategory.isFormat

@[inline]

def Unicode.GeneralCategory.isSurrogate (char : Char) : Bool

Check if surrogate character (Cs)

Unicode Property: General_Category=Cs

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isCs (char : Char) : Bool

Check if surrogate character (Cs)

Unicode Property: General_Category=Cs

Equations

• Unicode.GeneralCategory.isCs = Unicode.GeneralCategory.isSurrogate

@[inline]

def Unicode.GeneralCategory.isPrivateUse (char : Char) : Bool

Check if private use character (Co)

Unicode Property: General_Category=Co

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isCo (char : Char) : Bool

Check if private use character (Co)

Unicode Property: General_Category=Co

Equations

• Unicode.GeneralCategory.isCo = Unicode.GeneralCategory.isPrivateUse

@[inline]

def Unicode.GeneralCategory.isUnassigned (char : Char) : Bool

Check if unassigned character (Cn)

Unicode Property: General_Category=Cn

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.GeneralCategory.isCn (char : Char) : Bool

Check if unassigned character (Cn)

Unicode Property: General_Category=Cn

Equations

• Unicode.GeneralCategory.isCn = Unicode.GeneralCategory.isUnassigned

Case Type and Mapping

@[inline]

def Unicode.getLowerChar (char : Char) : Char

Map character to lowercase

This function does not handle the case where the lowercase mapping would consist of more than one character.

Unicode property: Simple_Lowercase_Mapping

Equations

• Unicode.getLowerChar char = match (Unicode.getUnicodeData char).lowercaseMapping with | some char => char | none => char

@[inline]

def Unicode.getUpperChar (char : Char) : Char

Map character to uppercase

This function does not handle the case where the uppercase mapping would consist of more than one character.

Unicode property: Simple_Uppercase_Mapping

Equations

• Unicode.getUpperChar char = match (Unicode.getUnicodeData char).uppercaseMapping with | some char => char | none => char

@[inline]

def Unicode.getTitleChar (char : Char) : Char

Map character to titlecase

This function does not handle the case where the titlecase mapping would consist of more than one character.

Unicode property: Simple_Titlecase_Mapping

Equations

• Unicode.getTitleChar char = match (Unicode.getUnicodeData char).titlecaseMapping with | some char => char | none => Unicode.getUpperChar char

Decomposition Type and Mapping

def Unicode.getCanonicalDecomposition (char : Char) : String

Get canonical decomposition of character (NFD)

Unicode property: Decomposition_Mapping

Equations

• Unicode.getCanonicalDecomposition char = { data := Unicode.getCanonicalDecomposition.loop [char] }

partial def Unicode.getCanonicalDecomposition.loop : List Char → List Char

Numeric Type and Value

@[inline]

def Unicode.isNumeric (char : Char) : Bool

Check if character represents a numerical value

Unicode property: Numeric_Type=Numeric

Equations

• One or more equations did not get rendered due to their size.

def Unicode.isNumeric.otherNumeric : Array UInt32

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isDigit (char : Char) : Bool

Check if character represents a digit in base 10

Unicode property: Numeric_Type=Digit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.getDigit? (char : Char) : Option (Fin 10)

Get value of digit

Unicode properties: Numeric_Value, Numeric_Type=Digit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isDecimal (char : Char) : Bool

Check if character represents a decimal digit

For this property, a character must be part of a contiguous sequence representing the ten decimal digits in order from 0 to 9.

Unicode property: Numeric_Type=Decimal

Equations

• Unicode.isDecimal char = match (Unicode.getUnicodeData char).numeric with | some (Unicode.NumericType.decimal value) => true | x => false

@[inline]

def Unicode.getDecimalRange? (char : Char) : Option (Char × Char)

Get decimal digit range

If the character is part of a contiguous sequence representing the ten decimal digits in order from 0 to 9, this function returns the first and last characters from this range.

Unicode property: Numeric_Type=Decimal

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isHexDigit (char : Char) : Bool

Check if character represents a digit in base 16

Unicode property: Hex_Digit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.getHexDigit? (char : Char) : Option (Fin 16)

Get value of digit

Unicode properties: Hex_Digit

Equations

• One or more equations did not get rendered due to their size.

Other Properties

@[inline]

def Unicode.isWhiteSpace (char : Char) : Bool

Check if white space character

Unicode property: White_Space

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isLowercase (char : Char) : Bool

Check if lowercase letter character

Unicode property: Lowercase

Equations

• Unicode.isLowercase char = (Unicode.GeneralCategory.isLl char || Unicode.PropList.isOtherLowercase char.val)

@[inline]

def Unicode.isUppercase (char : Char) : Bool

Check if uppercase letter character

Unicode property: Uppercase

Equations

• Unicode.isUppercase char = (Unicode.GeneralCategory.isLu char || Unicode.PropList.isOtherUppercase char.val)

@[inline]

def Unicode.isCased (char : Char) : Bool

Check if cased letter character

Unicode properties: Cased

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isCaseIgnorable (char : Char) : Bool

Check if character is ignorable for casing purposes

Generated from general categories Lm, Mn, Me, Sk, Cf, and word break properties MidLetter, MidNumLet, Single_Quote.

Unicode property: Case_Ignorable

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Unicode.isMath (char : Char) : Bool

Check if mathematical symbol character

Unicode property: Math

Equations

• Unicode.isMath char = (Unicode.GeneralCategory.isSm char || Unicode.PropList.isOtherMath char.val)

@[inline]

def Unicode.isAlphabetic (char : Char) : Bool

Check if alphabetic character

Unicode property: Alphabetic

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Unicode.isAlpha (char : Char) : Bool

Check if alphabetic character

Unicode property: Alphabetic

Equations

• Unicode.isAlpha = Unicode.isAlphabetic