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

Make UnicodeData for noncharacter code point

Equations

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

def Unicode.UnicodeData.mkControl (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for generic control code point

Equations

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

def Unicode.UnicodeData.mkSurrogate (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for generic surrogate code point

Equations

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

def Unicode.UnicodeData.mkPrivateUse (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for generic private use code point

Equations

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

def Unicode.UnicodeData.mkCJKCompatibilityIdeograph (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for CJK compatibilty ideograph code point

Equations

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

def Unicode.UnicodeData.mkCJKUnifiedIdeograph (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for CJK unified ideograph code point

Equations

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

def Unicode.UnicodeData.mkHangulSyllable (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for Hangul syllable code point

Equations

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

def Unicode.UnicodeData.mkTangutIdeograph (c : UInt32) : Unicode.UnicodeData

Make UnicodeData for Tangut ideograph code point

Equations

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

def Unicode.UnicodeData.txt : String

Raw string from file UnicodeData.txt

Equations

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

def Unicode.UnicodeData.data : Array Unicode.UnicodeData

Parsed data from UnicodeData.txt

Equations

• Unicode.UnicodeData.data = #[]

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

Get code point data from UnicodeData.txt

Equations

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

partial def Unicode.getUnicodeData?.find (code : UInt32) (lo hi : Nat) : Nat

Binary search

def Unicode.getUnicodeData! (code : UInt32) : Unicode.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) : Unicode.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 → Unicode.UnicodeData

instance Unicode.instInhabitedUnicodeDataStream : Inhabited Unicode.UnicodeDataStream

Equations

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

instance Unicode.instStreamUnicodeDataStreamUnicodeData : Stream Unicode.UnicodeDataStream Unicode.UnicodeData

Equations

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