structure Unicode.UnicodeData : Type

Structure for data from UnicodeData.txt

• code : UInt32

  Code Value

• name : Substring

  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 Unicode.instBEqUnicodeData : BEq UnicodeData

Equations

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

instance Unicode.instReprUnicodeData : Repr UnicodeData

Equations

• Unicode.instReprUnicodeData = { reprPrec := Unicode.instReprUnicodeData.repr }

def Unicode.instReprUnicodeData.repr : UnicodeData → Nat → Std.Format

Equations

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

@[reducible, inline, deprecated Unicode.UnicodeData.code (since := "1.2.0")]

abbrev Unicode.UnicodeData.codeValue (self : UnicodeData) : UInt32

Equations

• Unicode.UnicodeData.codeValue = Unicode.UnicodeData.code

@[reducible, inline, deprecated Unicode.UnicodeData.name (since := "1.2.0")]

abbrev Unicode.UnicodeData.characterName (self : UnicodeData) : Substring

Equations

• Unicode.UnicodeData.characterName = Unicode.UnicodeData.name

@[deprecated Unicode.UnicodeData.gc (since := "1.2.0")]

def Unicode.UnicodeData.generalCategory (d : UnicodeData) : GeneralCategory

Equations

• d.generalCategory = Unicode.GeneralCategory.ofGC! d.gc

@[reducible, inline, deprecated Unicode.UnicodeData.bidi (since := "1.2.0")]

abbrev Unicode.UnicodeData.bidiClass (self : UnicodeData) : BidiClass

Equations

• Unicode.UnicodeData.bidiClass = Unicode.UnicodeData.bidi

@[reducible, inline, deprecated Unicode.UnicodeData.cc (since := "1.2.0")]

abbrev Unicode.UnicodeData.canonicalCombiningClass (self : UnicodeData) : Nat

Equations

• Unicode.UnicodeData.canonicalCombiningClass = Unicode.UnicodeData.cc

@[reducible, inline, deprecated Unicode.UnicodeData.cc (since := "1.2.0")]

abbrev Unicode.UnicodeData.decompositionMapping (self : UnicodeData) : Option DecompositionMapping

Equations

• Unicode.UnicodeData.decompositionMapping = Unicode.UnicodeData.decomp

@[reducible, inline, deprecated Unicode.UnicodeData.lowercase (since := "1.2.0")]

abbrev Unicode.UnicodeData.lowercaseMapping (self : UnicodeData) : Option Char

Equations

• Unicode.UnicodeData.lowercaseMapping = Unicode.UnicodeData.lowercase

@[reducible, inline, deprecated Unicode.UnicodeData.uppercase (since := "1.2.0")]

abbrev Unicode.UnicodeData.uppercaseMapping (self : UnicodeData) : Option Char

Equations

• Unicode.UnicodeData.uppercaseMapping = Unicode.UnicodeData.uppercase

@[reducible, inline, deprecated Unicode.UnicodeData.titlecase (since := "1.2.0")]

abbrev Unicode.UnicodeData.titlecaseMapping (self : UnicodeData) : Option Char

Equations

• Unicode.UnicodeData.titlecaseMapping = Unicode.UnicodeData.titlecase

instance Unicode.instInhabitedUnicodeData : Inhabited UnicodeData

Equations

• Unicode.instInhabitedUnicodeData = { default := { code := 0, name := "<control-0000>".toSubstring, 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.

def Unicode.UnicodeData.mkControl (c : UInt32) : 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) : 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) : 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) : 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) : 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) : 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) : 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 UnicodeData

Parsed data from UnicodeData.txt

Equations

• Unicode.UnicodeData.data = #[]

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.

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

Binary search

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 Unicode.instInhabitedUnicodeDataStream : Inhabited UnicodeDataStream

Equations

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

def Unicode.instInhabitedUnicodeDataStream.default : UnicodeDataStream

Equations

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

instance Unicode.instStreamUnicodeDataStreamUnicodeData : Stream UnicodeDataStream UnicodeData

Equations

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