General API

As a general rule, for a given 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 performs the same calculation as the original but assumes that the input is in the domain; it may panic if this is not the case.

General Categories

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 either a non-titlecase letter or a separator.

The namespace Unicode.GeneralCategory provides a predicate for each general category, for example GeneralCategory.isLetter for GC.L and GeneralCategory.isMathSymbol for GC.Sm.

Scripts

Scripts are identified by their four-letter ISO 15924 codes using the type Script, for example Script.ofAbbrev! "Latn". The function getScript returns the script of a character and getScriptName? returns the long name of a script, such as "Latin". The function getScriptSet returns the ScriptSet of scripts a character is commonly used with; use ∈ to check membership, as in Script.ofAbbrev! "Grek" ∈ getScriptSet c.

Name

@[inline]

def Unicode.getName (char : Char) : String

Get character name

When the Unicode property Name is empty, a unique code point label is returned as recommended in Unicode Standard, section 4.8, for example <control-0009> or <private-use-E000>. 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

Returns Zzzz (Unknown) for unassigned, private use and noncharacter code points.

Unicode property: Script

Equations

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

@[inline]

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

Get script name

Returns the long name of the script, for example "Latin" for Latn. Returns none if the script code is not assigned to a script.

Unicode property: Script

Equations

• Unicode.getScriptName? s = Unicode.lookupScriptName s

@[inline]

def Unicode.getScriptSet (char : Char) : ScriptSet

Get the set of scripts a character is commonly used with

If Unicode lists no such set for the character, this contains only getScript char.

Note: despite its name, the Script_Extensions property does not extend the Script property. A set contains either one implicit script (Zyyy or Zinh) or one or more explicit scripts (UAX #24, Section 3.1). So a character whose script is Zyyy (Common) or Zinh (Inherited) may get a set that excludes its script: U+00B7 MIDDLE DOT has script Zyyy, but its set is Avst Cari Copt ….

Unicode property: Script_Extensions

Equations

• Unicode.getScriptSet char = Unicode.lookupScriptSet char.val

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 char ∈ cat to check whether a character belongs to a general category cat (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

@[instance_reducible]

instance Unicode.instMembershipCharGC : Membership Char GC

char ∈ cat holds when the general category of char is included in cat

Equations

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

@[instance_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 (LC = 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). It is not defined by Unicode but is provided for convenience.

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). It is not defined by Unicode but is provided for convenience.

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 final 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 category (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 character

This includes some characters that are not letters, such as U+24D0 CIRCLED LATIN SMALL LETTER A.

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 character

This includes some characters that are not letters, such as U+24B6 CIRCLED LATIN CAPITAL LETTER A.

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 character

This includes some characters that are not letters, such as U+24B6 CIRCLED LATIN CAPITAL LETTER A.

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 property values MidLetter, MidNumLet, Single_Quote.

Unicode property: Case_Ignorable

Equations

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

@[inline]

def Unicode.getLowerChar (char : Char) : Char

Map character to lowercase

Returns the character itself if it has no lowercase mapping. This function does not handle the case where the full lowercase mapping would consist of more than one character, for example U+0130 LATIN CAPITAL LETTER I WITH DOT ABOVE; use getLower for the full lowercase mapping.

Unicode property: Simple_Lowercase_Mapping

Equations

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

@[inline]

def Unicode.withLowercasing {β : Sort u_1} (char : Char) (k : Char → List Char → β) : β

Full lowercase mapping of a character, in continuation-passing style

Calls k with the first character of the full lowercase mapping of char and the list of its remaining characters. For example, for U+0130 LATIN CAPITAL LETTER I WITH DOT ABOVE, k is called with 'i' and ['\u0307']. Conditional mappings, such as for final sigma, are not applied.

Unicode property: Lowercase_Mapping

Equations

• Unicode.withLowercasing char k = match Unicode.unconsLowercasing✝ char with | (v, l) => k (Char.ofNat v.toNat) (List.map (fun (v : UInt32) => Char.ofNat v.toNat) l)

def Unicode.getLower (char : Char) : String

Full lowercase mapping of a character

The result may consist of more than one character, for example "i\u0307" for U+0130 LATIN CAPITAL LETTER I WITH DOT ABOVE. Conditional mappings, such as for final sigma, are not applied.

Unicode property: Lowercase_Mapping

Equations

• Unicode.getLower char = Unicode.withLowercasing char fun (c : Char) (l : List Char) => List.foldl String.push c.toString l

@[inline]

def Unicode.getUpperChar (char : Char) : Char

Map character to uppercase

Returns the character itself if it has no uppercase mapping. This function does not handle the case where the full uppercase mapping would consist of more than one character, for example U+00DF LATIN SMALL LETTER SHARP S; use getUpper for the full uppercase mapping.

Unicode property: Simple_Uppercase_Mapping

Equations

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

@[inline]

def Unicode.withUppercasing {β : Sort u_1} (char : Char) (k : Char → List Char → β) : β

Full uppercase mapping of a character, in continuation-passing style

Calls k with the first character of the full uppercase mapping of char and the list of its remaining characters. For example, for U+00DF LATIN SMALL LETTER SHARP S, k is called with 'S' and ['S']. Conditional mappings are not applied.

Unicode property: Uppercase_Mapping

Equations

• Unicode.withUppercasing char k = match Unicode.unconsUppercasing✝ char with | (v, u) => k (Char.ofNat v.toNat) (List.map (fun (v : UInt32) => Char.ofNat v.toNat) u)

def Unicode.getUpper (char : Char) : String

Full uppercase mapping of a character

The result may consist of more than one character, for example "SS" for U+00DF LATIN SMALL LETTER SHARP S. Conditional mappings are not applied.

Unicode property: Uppercase_Mapping

Equations

• Unicode.getUpper char = Unicode.withUppercasing char fun (c : Char) (u : List Char) => List.foldl String.push c.toString u

@[inline]

def Unicode.getTitleChar (char : Char) : Char

Map character to titlecase

Returns the character itself if it has no titlecase mapping. This function does not handle the case where the full titlecase mapping would consist of more than one character, for example U+00DF LATIN SMALL LETTER SHARP S; use getTitle for the full titlecase mapping.

Unicode property: Simple_Titlecase_Mapping

Equations

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

@[inline]

def Unicode.withTitlecasing {β : Sort u_1} (char : Char) (k : Char → List Char → β) : β

Full titlecase mapping of a character, in continuation-passing style

Calls k with the first character of the full titlecase mapping of char and the list of its remaining characters. For example, for U+00DF LATIN SMALL LETTER SHARP S, k is called with 'S' and ['s']. Conditional mappings are not applied.

Unicode property: Titlecase_Mapping

Equations

• Unicode.withTitlecasing char k = match Unicode.unconsTitlecasing✝ char with | (v, t) => k (Char.ofNat v.toNat) (List.map (fun (v : UInt32) => Char.ofNat v.toNat) t)

def Unicode.getTitle (char : Char) : String

Full titlecase mapping of a character

The result may consist of more than one character, for example "Ss" for U+00DF LATIN SMALL LETTER SHARP S. Conditional mappings are not applied.

Unicode property: Titlecase_Mapping

Equations

• Unicode.getTitle char = Unicode.withTitlecasing char fun (c : Char) (t : List Char) => List.foldl String.push c.toString t

@[inline]

def Unicode.getCaseFoldingChar (char : Char) : Char

Simple case folding of a character

Returns the character itself if it has no case folding. This function does not handle the case where case folding would consist of more than one character; use getCaseFolding for full case folding.

Unicode property: Simple_Case_Folding

Equations

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

@[inline]

def Unicode.withCaseFolding {β : Sort u_1} (char : Char) (k : Char → List Char → β) : β

Full case folding of a character, in continuation-passing style

Calls k with the first character of the full case folding of char and the list of its remaining characters. For example, for U+00DF LATIN SMALL LETTER SHARP S, k is called with 's' and ['s'].

Unicode property: Case_Folding

Equations

• Unicode.withCaseFolding char k = match Unicode.unconsCaseFolding✝ char with | (v, f) => k (Char.ofNat v.toNat) (List.map (fun (v : UInt32) => Char.ofNat v.toNat) f)

@[inline]

def Unicode.getCaseFolding (char : Char) : String

Full case folding of a character

The result may consist of more than one character, for example "ss" for U+00DF LATIN SMALL LETTER SHARP S.

Unicode property: Case_Folding

Equations

• Unicode.getCaseFolding char = Unicode.withCaseFolding char fun (c : Char) (f : List Char) => List.foldl String.push c.toString f

def Unicode.matchPrefixCaseInsensitive? (pat s : String.Slice) : Option (String.Slice × String.Slice)

Case-insensitive prefix match

If pat matches a prefix of s up to full case folding, returns that prefix and the rest of s. Otherwise, returns none. For example, "straße" matches "STRASSE", but "ß" does not match "S", since the full case folding of "ß" is "ss".

This is default caseless matching, as defined in the Unicode Standard; it does not normalize either string.

Unicode property: Case_Folding

Equations

• Unicode.matchPrefixCaseInsensitive? pat s = Unicode.matchPrefixCaseInsensitive?.loop✝ pat s s.startPos pat.startPos [] []

Decomposition Type and Mapping

def Unicode.getCanonicalCombiningClass (char : Char) : Nat

Get canonical combining class of character

Characters with combining class 0 are called starters. These include all characters that are not combining marks, as well as some combining marks.

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 full canonical decomposition of character (NFD)

Returns the full canonical decomposition of the character, including for Hangul syllables. Returns the character itself if it has no canonical decomposition.

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

Returns none if the character has no decomposition mapping. The tag field is none for a canonical mapping and some _ for a compatibility mapping. This is a single decomposition step, not the full decomposition 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

This includes decimal digits and other digits.

Unicode property: Numeric_Type (any value other than None)

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

This includes decimal digits as well as other digits such as U+00B2 SUPERSCRIPT TWO.

Unicode property: Numeric_Type=Decimal | 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

Returns none if the character is not a digit in the sense of isDigit.

Unicode properties: Numeric_Type=Decimal | 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

Returns none if the character is not a hexadecimal digit in the sense of isHexDigit. Both ASCII and fullwidth forms are accepted.

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 code point

Unicode property: Noncharacter_Code_Point

Equations

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

@[inline]

def Unicode.isDefaultIgnorableCodePoint (char : Char) : Bool

Check if default 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 char.val == 133 || Unicode.GeneralCategory.isSeparator char

@[inline]

def Unicode.isMath (char : Char) : Bool

Check if mathematical symbol character

Generated by General_Category=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 General_Category=L | General_Category=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 General_Category=L | General_Category=Nl | Other_Alphabetic.

Unicode property: Alphabetic

Equations

• Unicode.isAlpha = Unicode.isAlphabetic