structure Unicode.UnicodeData : Type

Structure for data from UnicodeData.txt

• code : UInt32

  Code Value

• name : String.Slice

  Character Name

• gc : GC

  General Category

• bidi : BidiClass

  Bidirectional Class

• cc : Nat

  Canonical Combining Class

• bidiMirrored : Bool

  Bidirectional Mirrored

• decomp : Option DecompositionMapping

  Character Decomposition Mapping

• numeric : Option NumericType

  Numeric Value

• uppercase : Option Char

  Uppercase Mapping

• lowercase : Option Char

  Lowercase Mapping

• titlecase : Option Char

  Titlecase Mapping

def Unicode.instBEqUnicodeData.beq : UnicodeData → UnicodeData → Bool

Equations

• One or more equations did not get rendered due to their size.
• Unicode.instBEqUnicodeData.beq x✝¹ x✝ = false

@[instance_reducible]

instance Unicode.instBEqUnicodeData : BEq UnicodeData

Equations

• Unicode.instBEqUnicodeData = { beq := Unicode.instBEqUnicodeData.beq }

@[instance_reducible]

instance Unicode.instInhabitedUnicodeData : Inhabited UnicodeData

Equations

• Unicode.instInhabitedUnicodeData = { default := { code := 0, name := "<control-0000>".toSlice, gc := Unicode.GC.Cc, bidi := Unicode.BidiClass.BN } }

def Unicode.UnicodeData.mkNoncharacter (code : UInt32) : UnicodeData

Make UnicodeData for a code point not listed in UnicodeData.txt

Such a code point is either a noncharacter or reserved (unassigned). Its name is the corresponding code point label, <noncharacter-NNNN> or <reserved-NNNN>, as specified in UAX #44, Section 4.2.5.

Equations

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

@[implemented_by _private.UnicodeData.Basic.0.Unicode.UnicodeData.dataImpl]

opaque Unicode.UnicodeData.data : Thunk (Array UnicodeData)

Parsed data from UnicodeData.txt

def Unicode.getUnicodeData? (code : UInt32) : Option UnicodeData

Get code point data from UnicodeData.txt

Equations

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

def Unicode.getUnicodeData! (code : UInt32) : UnicodeData

Get code point data from UnicodeData.txt

Equations

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

def Unicode.getUnicodeData (char : Char) : UnicodeData

Get character data from UnicodeData.txt

Equations

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

structure Unicode.UnicodeDataStream : Type

Stream type to roll through all code points up to Unicode.max, yielding UnicodeData

• code : UInt32
• index : USize
• default : UInt32 → UnicodeData

@[instance_reducible]

instance Unicode.instInhabitedUnicodeDataStream : Inhabited UnicodeDataStream

Equations

• Unicode.instInhabitedUnicodeDataStream = { default := Unicode.instInhabitedUnicodeDataStream.default }

def Unicode.UnicodeDataStream.next? (s : UnicodeDataStream) : Option (UnicodeData × UnicodeDataStream)

Equations

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

@[instance_reducible]

instance Unicode.instStreamUnicodeDataStreamUnicodeData : Std.Stream UnicodeDataStream UnicodeData

Equations

• Unicode.instStreamUnicodeDataStreamUnicodeData = { next? := Unicode.UnicodeDataStream.next? }