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.

Unicode general categories are encoded using the type GC. This type has a boolean algebra structure with inclusion ⊆, meet/intersection &&&, join/union ||| and complement ~~~. The relation ∈ is provided to check whether a character belongs to a given category. For example, c ∈ (GC.L &&& ~~~GC.Lt) ||| GC.Z checks whether c is a either a non-titlecase letter or a separator.

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 recommended 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

Script

@[inline]

def Unicode.getScript (char : Char) : Script

Get character script

Unicode property: Script

Equations

• Unicode.getScript char = Unicode.lookupScript char.val

@[inline]

def Unicode.getScriptName? (s : Script) : Option String

Get script name

Returns none if the script code is unassigned.

Unicode property: Script

Equations

• Unicode.getScriptName? s = Option.map toString (Unicode.lookupScriptName s)

Bidirectional Properties

@[inline]

def Unicode.getBidiClass (char : Char) : 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.getGC (char : Char) : GC

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.getGC char = if h : char.toNat < Unicode.getGC.table✝.size then Unicode.getGC.table✝[char.toNat] else Unicode.lookupGC char.val

@[implicit_reducible]

instance Unicode.instMembershipCharGC : Membership Char GC

Equations

• Unicode.instMembershipCharGC = { mem := fun (cat : Unicode.GC) (char : Char) => Unicode.getGC char ⊆ cat }

@[implicit_reducible]

instance Unicode.instDecidableMemCharGC (char : Char) (cat : GC) : Decidable (char ∈ cat)

Equations

• Unicode.instDecidableMemCharGC char cat = (Unicode.getGC char).instDecidableSubset cat

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.L)

@[reducible, inline]

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

Check if lowercase letter character (Ll)

Unicode Property: General_Category=Ll

Equations

• Unicode.GeneralCategory.isLowercaseLetter char = decide (char ∈ Unicode.GC.Ll)

@[reducible, inline]

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

Check if titlecase letter character (Lt)

Unicode Property: General_Category=Lt

Equations

• Unicode.GeneralCategory.isTitlecaseLetter char = decide (char ∈ Unicode.GC.Lt)

@[reducible, inline]

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

Check if uppercase letter character (Lu)

Unicode Property: General_Category=Lu

Equations

• Unicode.GeneralCategory.isUppercaseLetter char = decide (char ∈ Unicode.GC.Lu)

@[reducible, inline]

abbrev 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

• Unicode.GeneralCategory.isCasedLetter char = decide (char ∈ Unicode.GC.LC)

@[reducible, inline]

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

Check if modifier letter character (Lm)

Unicode Property: General_Category=Lm

Equations

• Unicode.GeneralCategory.isModifierLetter char = decide (char ∈ Unicode.GC.Lm)

@[reducible, inline]

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

Check if other letter character (Lo)

Unicode Property: General_Category=Lo

Equations

• Unicode.GeneralCategory.isOtherLetter char = decide (char ∈ Unicode.GC.Lo)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.M)

@[reducible, inline]

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

Check if nonspacing combining mark character (Mn)

Unicode Property: General_Category=Mn

Equations

• Unicode.GeneralCategory.isNonspacingMark char = decide (char ∈ Unicode.GC.Mn)

@[reducible, inline]

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

Check if spacing combining mark character (Mc)

Unicode Property: General_Category=Mc

Equations

• Unicode.GeneralCategory.isSpacingMark char = decide (char ∈ Unicode.GC.Mc)

@[reducible, inline]

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

Check if enclosing combining mark character (Me)

Unicode Property: General_Category=Me

Equations

• Unicode.GeneralCategory.isEnclosingMark char = decide (char ∈ Unicode.GC.Me)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.N)

@[reducible, inline]

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

Check if decimal number character (Nd)

Unicode Property: General_Category=Nd

Equations

• Unicode.GeneralCategory.isDecimalNumber char = decide (char ∈ Unicode.GC.Nd)

@[reducible, inline]

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

Check if letter number character (Nl)

Unicode Property: General_Category=Nl

Equations

• Unicode.GeneralCategory.isLetterNumber char = decide (char ∈ Unicode.GC.Nl)

@[reducible, inline]

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

Check if other number character (No)

Unicode Property: General_Category=No

Equations

• Unicode.GeneralCategory.isOtherNumber char = decide (char ∈ Unicode.GC.No)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.P)

@[reducible, inline]

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

Check if connector punctuation character (Pc)

Unicode Property: General_Category=Pc

Equations

• Unicode.GeneralCategory.isConnectorPunctuation char = decide (char ∈ Unicode.GC.Pc)

@[reducible, inline]

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

Check if dash punctuation character (Pd)

Unicode Property: General_Category=Pd

Equations

• Unicode.GeneralCategory.isDashPunctuation char = decide (char ∈ Unicode.GC.Pd)

@[reducible, inline]

abbrev 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

Equations

• Unicode.GeneralCategory.isGroupPunctuation char = decide (char ∈ Unicode.GC.PG)

@[reducible, inline]

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

Check if open punctuation character (Ps)

Unicode Property: General_Category=Ps

Equations

• Unicode.GeneralCategory.isOpenPunctuation char = decide (char ∈ Unicode.GC.Ps)

@[reducible, inline]

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

Check if close punctuation character (Pe)

Unicode Property: General_Category=Pe

Equations

• Unicode.GeneralCategory.isClosePunctuation char = decide (char ∈ Unicode.GC.Pe)

@[reducible, inline]

abbrev 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

Equations

• Unicode.GeneralCategory.isQuotePunctuation char = decide (char ∈ Unicode.GC.PQ)

@[reducible, inline]

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

Check if initial punctuation character (Pi)

Unicode Property: General_Category=Pi

Equations

• Unicode.GeneralCategory.isInitialPunctuation char = decide (char ∈ Unicode.GC.Pi)

@[reducible, inline]

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

Check if initial punctuation character (Pf)

Unicode Property: General_Category=Pf

Equations

• Unicode.GeneralCategory.isFinalPunctuation char = decide (char ∈ Unicode.GC.Pf)

@[reducible, inline]

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

Check if other punctuation character (Po)

Unicode Property: General_Category=Po

Equations

• Unicode.GeneralCategory.isOtherPunctuation char = decide (char ∈ Unicode.GC.Po)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.S)

@[reducible, inline]

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

Check if math symbol character (Sm)

Unicode Property: General_Category=Sm

Equations

• Unicode.GeneralCategory.isMathSymbol char = decide (char ∈ Unicode.GC.Sm)

@[reducible, inline]

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

Check if currency symbol character (Sc)

Unicode Property: General_Category=Sc

Equations

• Unicode.GeneralCategory.isCurrencySymbol char = decide (char ∈ Unicode.GC.Sc)

@[reducible, inline]

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

Check if modifier symbol character (Sk)

Unicode Property: General_Category=Sk

Equations

• Unicode.GeneralCategory.isModifierSymbol char = decide (char ∈ Unicode.GC.Sk)

@[reducible, inline]

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

Check if other symbol character (So)

Unicode Property: General_Category=So

Equations

• Unicode.GeneralCategory.isOtherSymbol char = decide (char ∈ Unicode.GC.So)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.Z)

@[reducible, inline]

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

Check if space separator character (Zs)

Unicode Property: General_Category=Zs

Equations

• Unicode.GeneralCategory.isSpaceSeparator char = decide (char ∈ Unicode.GC.Zs)

@[reducible, inline]

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

Check if line separator character (Zl)

Unicode Property: General_Category=Zl

Equations

• Unicode.GeneralCategory.isLineSeparator char = decide (char ∈ Unicode.GC.Zl)

@[reducible, inline]

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

Check if paragraph separator character (Zp)

Unicode Property: General_Category=Zp

Equations

• Unicode.GeneralCategory.isParagraphSeparator char = decide (char ∈ Unicode.GC.Zp)

@[reducible, inline]

abbrev 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 = decide (char ∈ Unicode.GC.C)

@[reducible, inline]

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

Check if control character (Cc)

Unicode Property: General_Category=Cc

Equations

• Unicode.GeneralCategory.isControl char = decide (char ∈ Unicode.GC.Cc)

@[reducible, inline]

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

Check if format character (Cf)

Unicode Property: General_Category=Cf

Equations

• Unicode.GeneralCategory.isFormat char = decide (char ∈ Unicode.GC.Cf)

@[reducible, inline]

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

Check if surrogate character (Cs)

Does not actually occur since Lean does not regard surrogate code points as characters.

Unicode Property: General_Category=Cs

Equations

• Unicode.GeneralCategory.isSurrogate char = decide (char ∈ Unicode.GC.Cs)

@[reducible, inline]

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

Check if private use character (Co)

Unicode Property: General_Category=Co

Equations

• Unicode.GeneralCategory.isPrivateUse char = decide (char ∈ Unicode.GC.Co)

@[reducible, inline]

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

Check if unassigned character (Cn)

Unicode Property: General_Category=Cn

Equations

• Unicode.GeneralCategory.isUnassigned char = decide (char ∈ Unicode.GC.Cn)

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

Equations

• Unicode.isCaseIgnorable char = (decide (char ∈ Unicode.GC.Lm ||| Unicode.GC.Mn ||| Unicode.GC.Sk ||| Unicode.GC.Cf) || List.elem char.val Unicode.isCaseIgnorable.other✝)

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

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

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 a hexadecimal digit

Unicode property: Hex_Digit

Equations

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

Other Properties

@[inline]

def Unicode.isNoncharacterCodePoint (char : Char) : Bool

Check if noncharacter

Unicode property: Noncharacter_Code_Point

Equations

• Unicode.isNoncharacterCodePoint char = Unicode.lookupNoncharacterCodePoint char.val

@[inline]

def Unicode.isDefaultIgnorableCodePoint (char : Char) : Bool

Check if ignorable character

Unicode property: Default_Ignorable_Code_Point

Equations

• Unicode.isDefaultIgnorableCodePoint char = Unicode.lookupDefaultIgnorableCodePoint char.val

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