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.lookupName char.val

Bidirectional Properties

@[inline]

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

Get character bidirectional class

Unicode property: Bidi_Class

Equations

• Unicode.getBidiClass char = Unicode.lookupBidiClass char.val

@[inline]

def Unicode.isBidiMirrored (char : Char) : Bool

Check if bidirectional mirrored character

Unicode property: Bidi_Mirrored

Equations

• Unicode.isBidiMirrored char = Unicode.lookupBidiMirrored char.val

@[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 = if h : char.toNat < Unicode.getGeneralCategory.table.size then Unicode.getGeneralCategory.table[char.toNat] else Unicode.lookupGeneralCategory char.val

def Unicode.getGeneralCategory.str : String

Equations

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

def Unicode.getGeneralCategory.table : Array Unicode.GeneralCategory

Equations

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

@[inline]

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

Check if character belongs to the general category

Unicode property: General_Category

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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.isGroupPunctuation (char : Char) : Bool

Check if grouping punctuation character (PG)

This is a derived category (PG = Ps | Pe).

Unicode Property: General_Category=PG

@[reducible, inline]

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

Check if grouping punctuation character (PG)

This is a derived category (PG = Ps | Pe).

Unicode Property: General_Category=PG

Equations

• Unicode.GeneralCategory.isPG = Unicode.GeneralCategory.isGroupPunctuation

@[inline]

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

Check if open punctuation character (Ps)

Unicode Property: General_Category=Ps

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

@[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.isQuotePunctuation (char : Char) : Bool

Check if quoting punctuation character (PQ)

This is a derived category (PQ = Pi | Pf).

Unicode Property: General_Category=PQ

@[reducible, inline]

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

Check if quoting punctuation character (PQ)

This is a derived category (PQ = Pi | Pf).

Unicode Property: General_Category=PQ

Equations

• Unicode.GeneralCategory.isPQ = Unicode.GeneralCategory.isQuotePunctuation

@[inline]

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

Check if initial punctuation character (Pi)

Unicode Property: General_Category=Pi

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[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.isLowercase (char : Char) : Bool

Check if lowercase letter character

Generated by General_Category=Ll | Other_Lowercase.

Unicode property: Lowercase

Equations

• Unicode.isLowercase char = if char.val < 128 then decide ('a' ≤ char) && decide (char ≤ 'z') else Unicode.lookupLowercase char.val

@[inline]

def Unicode.isUppercase (char : Char) : Bool

Check if uppercase letter character

Generated by General_Category=Lu | Other_Uppercase.

Unicode property: Uppercase

Equations

• Unicode.isUppercase char = if char.val < 128 then decide ('A' ≤ char) && decide (char ≤ 'Z') else Unicode.lookupUppercase char.val

@[inline]

def Unicode.isCased (char : Char) : Bool

Check if cased letter character

Generated by General_Category=LC | Other_Lowercase | Other_Uppercase.

Unicode property: Cased

Equations

• Unicode.isCased char = if char.val < 128 then decide ('A' ≤ char) && decide (char ≤ 'Z') || decide ('a' ≤ char) && decide (char ≤ 'z') else Unicode.lookupCased char.val

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

def Unicode.isCaseIgnorable.other : List UInt32

Auxiliary data for isCaseIgnorable

Extracted from UCD auxiliary/WordBreakProperty.txt.

Equations

• Unicode.isCaseIgnorable.other = [39, 46, 58, 183, 903, 1375, 1524, 8216, 8217, 8231, 8228, 65043, 65109, 65106, 65287, 65294, 65306]

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

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

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

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

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

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

Decomposition Type and Mapping

def Unicode.getCanonicalCombiningClass (char : Char) : Nat

Get canonical combining class of character

Unicode property: Canonical_Combining_Class

Equations

• Unicode.getCanonicalCombiningClass char = if char.val < 128 then 0 else Unicode.lookupCanonicalCombiningClass char.val

def Unicode.getCanonicalDecomposition (char : Char) : String

Get canonical decomposition of character (NFD)

Unicode properties: Decomposition_Mapping Decomposition_Type=Canonical

Equations

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

def Unicode.getDecompositionMapping? (char : Char) : Option Unicode.DecompositionMapping

Get decomposition mapping of a character

This is used in normalization to canonical decomposition (NFD) and compatibility decomposition (NFKD).

Unicode properties: Decomposition_Type Decomposition_Mapping

Equations

• Unicode.getDecompositionMapping? char = if char.val < 128 then none else Unicode.lookupDecompositionMapping? char.val

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_Type=Digit Numeric_Value

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

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

@[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 properties: Numeric_Type=Decimal Numeric_Value

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 property: 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

• Unicode.isWhiteSpace char = if char.val < 128 then char == ' ' || decide (char ≥ '\t') && decide (char ≤ '\x0d') else Unicode.GeneralCategory.isSeparator char

@[inline]

def Unicode.isMath (char : Char) : Bool

Check if mathematical symbol character

Generated by GeneralCategory=Sm | Other_Math.

Unicode property: Math

Equations

• Unicode.isMath char = Unicode.lookupMath char.val

@[inline]

def Unicode.isAlphabetic (char : Char) : Bool

Check if alphabetic character

Generated by GeneralCategory=L | GeneralCategory=Nl | Other_Alphabetic.

Unicode property: Alphabetic

Equations

• Unicode.isAlphabetic char = if char.val < 128 then decide ('A' ≤ char) && decide (char ≤ 'Z') || decide ('a' ≤ char) && decide (char ≤ 'z') else Unicode.lookupAlphabetic char.val

@[reducible, inline]

abbrev Unicode.isAlpha (char : Char) : Bool

Check if alphabetic character

Generated by GeneralCategory=L | GeneralCategory=Nl | Other_Alphabetic.

Unicode property: Alphabetic

Equations

• Unicode.isAlpha = Unicode.isAlphabetic