@[extern unicode_case_lookup]

opaque Unicode.CLib.lookupCase (c : UInt32) : UInt64

@[reducible, inline]

abbrev Unicode.CLib.oUpper : UInt64

Equations

• Unicode.CLib.oUpper = 4294967296

@[reducible, inline]

abbrev Unicode.CLib.oLower : UInt64

Equations

• Unicode.CLib.oLower = 8589934592

@[reducible, inline]

abbrev Unicode.CLib.oAlpha : UInt64

Equations

• Unicode.CLib.oAlpha = 17179869184

@[reducible, inline]

abbrev Unicode.CLib.oMath : UInt64

Equations

• Unicode.CLib.oMath = 34359738368

@[extern unicode_prop_lookup]

opaque Unicode.CLib.lookupProp (c : UInt32) : UInt64

def Unicode.lookupBidiClass (c : UInt32) : BidiClass

Get bidirectional class using lookup table

Unicode property: Bidi_Class

Equations

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

def Unicode.lookupBidiClass.str : String

Equations

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

def Unicode.lookupBidiClass.table : Thunk (Array (UInt32 × UInt32 × BidiClass))

Equations

• Unicode.lookupBidiClass.table = Unicode.parseDataTable✝ Unicode.lookupBidiClass.str fun (x x : UInt32) (x : Array Substring) => Unicode.BidiClass.ofAbbrev! x[0]!

def Unicode.lookupCanonicalCombiningClass (c : UInt32) : Nat

Get canonical combining class using lookup table

Unicode property: Canonical_Combining_Class

Equations

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

def Unicode.lookupCanonicalCombiningClass.str : String

Equations

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

def Unicode.lookupCanonicalCombiningClass.table : Thunk (Array (UInt32 × UInt32 × Nat))

Equations

• Unicode.lookupCanonicalCombiningClass.table = Unicode.parseDataTable✝ Unicode.lookupCanonicalCombiningClass.str fun (x x : UInt32) (x : Array Substring) => x[0]!.toNat?.get!

def Unicode.lookupCanonicalDecompositionMapping (c : UInt32) : List UInt32

Get canonical decomposition mapping using lookup table

Unicode properties: Decomposition_Mapping Decomposition_Type=Canonical

Equations

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

def Unicode.lookupCanonicalDecompositionMapping.str : String

Equations

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

def Unicode.lookupCanonicalDecompositionMapping.table : Thunk (Array (UInt32 × List UInt32))

Equations

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

def Unicode.lookupCaseMapping (c : UInt32) : UInt32 × UInt32 × UInt32

Get simple case mappings of a code point using lookup table

Unicode properties: Simple_Lowercase_Mapping Simple_Uppercase_Mapping Simple_Titlecase_Mapping

Equations

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

def Unicode.lookupDecompositionMapping? (c : UInt32) : Option DecompositionMapping

Get decomposition mapping using lookup table

Unicode properties: Decomposition_Mapping Decomposition_Type

Equations

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

def Unicode.lookupDecompositionMapping?.str : String

Equations

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

def Unicode.lookupDecompositionMapping?.table : Thunk (Array (UInt32 × Option CompatibilityTag × Array UInt32))

Equations

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

@[inline]

def Unicode.lookupGC (c : UInt32) : GC

Get general category of a code point using lookup table

Unicode property: General_Category

Equations

• Unicode.lookupGC c = (Unicode.CLib.lookupProp c).toUInt32

@[inline, deprecated Unicode.lookupGC (since := "v1.3.0")]

def Unicode.lookupGeneralCategory (c : UInt32) : GeneralCategory

Equations

• Unicode.lookupGeneralCategory c = Unicode.GeneralCategory.ofGC! (Unicode.lookupGC c)

def Unicode.lookupName (c : UInt32) : String

Get name of a code point using lookup table

Unicode property: Name

Equations

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

def Unicode.lookupName.str : String

Equations

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

def Unicode.lookupName.table : Thunk (Array (UInt32 × UInt32 × Substring))

Equations

• Unicode.lookupName.table = Unicode.parseDataTable✝ Unicode.lookupName.str fun (x x : UInt32) (x : Array Substring) => x[0]!

def Unicode.lookupNumericValue (c : UInt32) : Option NumericType

Get numeric value of a code point using lookup table

Unicode properties: Numeric_Type Numeric_Value

Equations

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

def Unicode.lookupNumericValue.str : String

Equations

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

def Unicode.lookupNumericValue.table : Thunk (Array (UInt32 × UInt32 × NumericType))

Equations

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

def Unicode.lookupOther (c : UInt32) : UInt32

Get other properties using lookup table

Unicode properties: Other_Alphabetic, Other_Lowercase, Other_Uppercase, Other_Math

Equations

• Unicode.lookupOther c = (Unicode.CLib.lookupProp c >>> 32).toUInt32

Properties

@[inline]

def Unicode.lookupAlphabetic (c : UInt32) : Bool

Check if code point is alphabetic using lookup table

Unicode property: Alphabetic

Equations

• Unicode.lookupAlphabetic c = (Unicode.CLib.lookupProp c &&& (Unicode.CLib.oAlpha ||| UInt32.toUInt64 (Unicode.GC.L ||| Unicode.GC.Nl)) != 0)

def Unicode.lookupBidiMirrored (c : UInt32) : Bool

Check if code point is bidi mirrored using lookup table

Unicode property: Bidi_Mirrored

Equations

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

def Unicode.lookupBidiMirrored.str : String

Equations

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

def Unicode.lookupBidiMirrored.table : Thunk (Array (UInt32 × UInt32))

Equations

• Unicode.lookupBidiMirrored.table = Unicode.parsePropTable✝ Unicode.lookupBidiMirrored.str

@[inline]

def Unicode.lookupCased (c : UInt32) : Bool

Check if code point is a cased letter using lookup table

Unicode property: Cased

Equations

• Unicode.lookupCased c = (Unicode.CLib.lookupProp c &&& (Unicode.CLib.oUpper ||| Unicode.CLib.oLower ||| UInt32.toUInt64 Unicode.GC.LC) != 0)

@[inline]

def Unicode.lookupLowercase (c : UInt32) : Bool

Check if code point is a lowercase letter using lookup table

Unicode property: Lowercase

Equations

• Unicode.lookupLowercase c = (Unicode.CLib.lookupProp c &&& (Unicode.CLib.oLower ||| UInt32.toUInt64 Unicode.GC.Ll) != 0)

@[inline]

def Unicode.lookupMath (c : UInt32) : Bool

Check if code point is a mathematical symbol using lookup table

Unicode property: Math

Equations

• Unicode.lookupMath c = (Unicode.CLib.lookupProp c &&& (Unicode.CLib.oMath ||| UInt32.toUInt64 Unicode.GC.Sm) != 0)

@[inline]

def Unicode.lookupTitlecase (c : UInt32) : Bool

Check if code point is a titlecase letter using lookup table

Unicode property: Titlecase

Equations

• Unicode.lookupTitlecase c = (Unicode.lookupGC c == Unicode.GC.Lt)

@[inline]

def Unicode.lookupUppercase (c : UInt32) : Bool

Check if code point is a uppercase letter using lookup table

Unicode property: Uppercase

Equations

• Unicode.lookupUppercase c = (Unicode.CLib.lookupProp c &&& (Unicode.CLib.oUpper ||| UInt32.toUInt64 Unicode.GC.Lu) != 0)

def Unicode.lookupWhiteSpace (c : UInt32) : Bool

Check if code point is a white space character using lookup table

Unicode property: White_Space

Equations

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

def Unicode.lookupWhiteSpace.str : String

Equations

• Unicode.lookupWhiteSpace.str = "0009;000D\n0020;\n0085;\n00A0;\n1680;\n2000;200A\n2028;\n2029;\n202F;\n205F;\n3000;\n"

def Unicode.lookupWhiteSpace.table : Thunk (Array (UInt32 × UInt32))

Equations

• Unicode.lookupWhiteSpace.table = Unicode.parsePropTable✝ Unicode.lookupWhiteSpace.str