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

@[implicit_reducible]

instance Unicode.instBEqUnicodeData : BEq UnicodeData

Equations

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

@[implicit_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 noncharacter code point

Equations

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

opaque Unicode.UnicodeData.data : Array UnicodeData

Parse 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

def Unicode.instInhabitedUnicodeDataStream.default : UnicodeDataStream

Equations

• Unicode.instInhabitedUnicodeDataStream.default = { code := default, index := default, default := default }

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

@[implicit_reducible]

instance Unicode.instStreamUnicodeDataStreamUnicodeData : Std.Stream UnicodeDataStream UnicodeData

Equations

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