unsafe def Char.mkUnsafe : UInt32 → Char

Low-level conversion from UInt32 to Char (unsafe)

This function translates to a no-op in the compiler. However, it does not check whether the UInt32 code is a valid Char value. Only use where it's known for external reasons that the code is valid.

Equations

• Char.mkUnsafe = unsafeCast

def Unicode.instCoeStringSubstring_unicodeBasic : Coe String Substring

Coercion from String to Substring

This coercion is in Std but not in Lean core. It is scoped to Unicode here to avoid issues in low-level packages that don't use Std.

Equations

• Unicode.instCoeStringSubstring_unicodeBasic = { coe := String.toSubstring }

def Unicode.max : UInt32

Maximum valid code point value

Equations

• Unicode.max = 1114111

def Unicode.toHexStringAux (code : UInt32) : String

Hexadecimal string representation of a code point

Same as toHexString but without the U+ prefix.

Equations

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

@[inline]

def Unicode.toHexString (code : UInt32) : String

Hexadecimal string representation of a code point

Prefix U+ followed by at least four uppercase hexadecimal digits (e.g. U+0123 and U+4B0A1 but neither U+123 nor U+4b0a1).

Equations

• Unicode.toHexString code = "U+" ++ Unicode.toHexStringAux code

def Unicode.ofHexString? (str : Substring) : Option UInt32

Get code point from hexadecimal string representation

For convenience, the U+ prefix may be omitted and lowercase hexadecimal digits are accepted.

Equations

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

@[inline]

def Unicode.ofHexString?.hexValue? (dgt : Char) : Option UInt32

Get value of hex digit

Equations

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

def Unicode.ofHexString! (str : Substring) : UInt32

Get code point from hexadecimal string representation

For convenience, the U+ prefix may be omitted and lowercase hexadecimal digits are accepted.

Equations

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

General Category

inductive Unicode.MajorGeneralCategory : Type

Major general category (L, M, N, P, S, Z, C)

Unicode property: General_Category

• letter: Unicode.MajorGeneralCategory

  (L) Letter

• mark: Unicode.MajorGeneralCategory

  (M) Mark

• number: Unicode.MajorGeneralCategory

  (N) Number

• punctuation: Unicode.MajorGeneralCategory

  (P) Punctuation

• symbol: Unicode.MajorGeneralCategory

  (S) Symbol

• separator: Unicode.MajorGeneralCategory

  (Z) Separator

• other: Unicode.MajorGeneralCategory

  (C) Other

instance Unicode.instInhabitedMajorGeneralCategory : Inhabited Unicode.MajorGeneralCategory

Equations

• Unicode.instInhabitedMajorGeneralCategory = { default := Unicode.MajorGeneralCategory.letter }

instance Unicode.instDecidableEqMajorGeneralCategory : DecidableEq Unicode.MajorGeneralCategory

Equations

• Unicode.instDecidableEqMajorGeneralCategory x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Unicode.MajorGeneralCategory.toAbbrev : Unicode.MajorGeneralCategory → String

String abbreviation for major general category

Equations

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

inductive Unicode.MinorGeneralCategory : Unicode.MajorGeneralCategory → Type

Minor general category

Unicode property: General_Category

• casedLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (LC) cased letter (derived from Lu | Ll | Lt)

• uppercaseLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (Lu) uppercase letter

• lowercaseLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (Ll) lowercase letter

• titlecaseLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (Lt) titlecase letter: digraphic character, with first part uppercase

• modifierLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (Lm) modifier letter

• otherLetter: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.letter

  (Lo) other letters, including syllables and ideographs

• nonspacingMark: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.mark

  (Mn) nonspacing combining mark (zero advance width)

• spacingMark: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.mark

  (Mc) spacing combining mark (positive advance width)

• enclosingMark: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.mark

  (Me) enclosing combining mark

• decimalNumber: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.number

  (Nd) decimal digit

• letterNumber: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.number

  (Nl) letter number: a letterlike numeric character

• otherNumber: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.number

  (No) numeric character of other type

• connectorPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Pc) connecting punctuation mark, like a tie

• dashPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Pd) dash or hyphen punctuation mark

• openPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Ps) opening punctuation mark (of a pair)

• closePunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Pe) closing punctuation mark (of a pair)

• initialPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Pi) initial quotation mark

• finalPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Pf) final quotation mark

• otherPunctuation: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.punctuation

  (Po) punctuation mark of other type

• mathSymbol: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.symbol

  (Sm) symbol of mathematical use

• currencySymbol: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.symbol

  (Sc) currency sign

• modifierSymbol: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.symbol

  (Sk) non-letterlike modifier symbol

• otherSymbol: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.symbol

  (So) symbol of other type

• spaceSeparator: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.separator

  (Zs) space character (of various non-zero widths)

• lineSeparator: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.separator

  (Zl) line separator (U+2028 LINE SEPARATOR only)

• paragraphSeparator: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.separator

  (Zp) paragraph separator (U+2029 PARAGRAPH SEPARATOR only)

• control: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.other

  (Cc) C0 or C1 control code

• format: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.other

  (Cf) format control character

• surrogate: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.other

  (Cs) surrogate code point

• privateUse: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.other

  (Co) private-use character

• unassigned: Unicode.MinorGeneralCategory Unicode.MajorGeneralCategory.other

  (Cn) reserved unassigned code point or a noncharacter

instance Unicode.instDecidableEqMinorGeneralCategory : {a : Unicode.MajorGeneralCategory} → DecidableEq (Unicode.MinorGeneralCategory a)

Equations

• Unicode.instDecidableEqMinorGeneralCategory = Unicode.decEqMinorGeneralCategory✝

structure Unicode.GeneralCategory : Type

General category of a code point

Unicode property: General_Category

• major : Unicode.MajorGeneralCategory

  Major general category of a code point

• minor : Option (Unicode.MinorGeneralCategory self.major)

  Minor general category of a code point

instance Unicode.instInhabitedGeneralCategory : Inhabited Unicode.GeneralCategory

Equations

• Unicode.instInhabitedGeneralCategory = { default := { major := default, minor := default } }

instance Unicode.instDecidableEqGeneralCategory : DecidableEq Unicode.GeneralCategory

Equations

• Unicode.instDecidableEqGeneralCategory = Unicode.decEqGeneralCategory✝

def Unicode.GeneralCategory.L : Unicode.GeneralCategory

General category: letter (L)

Equations

• Unicode.GeneralCategory.L = { major := Unicode.MajorGeneralCategory.letter, minor := none }

def Unicode.GeneralCategory.LC : Unicode.GeneralCategory

General category: cased letter (LC)

Equations

• Unicode.GeneralCategory.LC = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.casedLetter }

def Unicode.GeneralCategory.Lu : Unicode.GeneralCategory

General category: uppercase letter (Lu)

Equations

• Unicode.GeneralCategory.Lu = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.uppercaseLetter }

def Unicode.GeneralCategory.Ll : Unicode.GeneralCategory

General category: lowercase letter (Ll)

Equations

• Unicode.GeneralCategory.Ll = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.lowercaseLetter }

def Unicode.GeneralCategory.Lt : Unicode.GeneralCategory

General category: titlecase letter (Lt)

Equations

• Unicode.GeneralCategory.Lt = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.titlecaseLetter }

def Unicode.GeneralCategory.Lm : Unicode.GeneralCategory

General category: modifier letter (Lm)

Equations

• Unicode.GeneralCategory.Lm = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.modifierLetter }

def Unicode.GeneralCategory.Lo : Unicode.GeneralCategory

General category: other letter (Lo)

Equations

• Unicode.GeneralCategory.Lo = { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.otherLetter }

def Unicode.GeneralCategory.M : Unicode.GeneralCategory

General category mark (M)

Equations

• Unicode.GeneralCategory.M = { major := Unicode.MajorGeneralCategory.mark, minor := none }

def Unicode.GeneralCategory.Mn : Unicode.GeneralCategory

General category: nonspacing combining mark (Mn)

Equations

• Unicode.GeneralCategory.Mn = { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.nonspacingMark }

def Unicode.GeneralCategory.Mc : Unicode.GeneralCategory

General category: spacing combining mark (Mc)

Equations

• Unicode.GeneralCategory.Mc = { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.spacingMark }

def Unicode.GeneralCategory.Me : Unicode.GeneralCategory

General category: enclosing combining mark (Me)

Equations

• Unicode.GeneralCategory.Me = { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.enclosingMark }

def Unicode.GeneralCategory.N : Unicode.GeneralCategory

General category: number (N)

Equations

• Unicode.GeneralCategory.N = { major := Unicode.MajorGeneralCategory.number, minor := none }

def Unicode.GeneralCategory.Nd : Unicode.GeneralCategory

General category: decimal digit (Nd)

Equations

• Unicode.GeneralCategory.Nd = { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.decimalNumber }

def Unicode.GeneralCategory.Nl : Unicode.GeneralCategory

General category: letter number (Nl)

Equations

• Unicode.GeneralCategory.Nl = { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.letterNumber }

def Unicode.GeneralCategory.No : Unicode.GeneralCategory

General category: other number (No)

Equations

• Unicode.GeneralCategory.No = { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.otherNumber }

def Unicode.GeneralCategory.P : Unicode.GeneralCategory

General category: punctuation (P)

Equations

• Unicode.GeneralCategory.P = { major := Unicode.MajorGeneralCategory.punctuation, minor := none }

def Unicode.GeneralCategory.Pc : Unicode.GeneralCategory

General category: connector punctuation (Pc)

Equations

• Unicode.GeneralCategory.Pc = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.connectorPunctuation }

def Unicode.GeneralCategory.Pd : Unicode.GeneralCategory

General category: dash punctuation (Pd)

Equations

• Unicode.GeneralCategory.Pd = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.dashPunctuation }

def Unicode.GeneralCategory.Ps : Unicode.GeneralCategory

General category: opening punctuation (Ps)

Equations

• Unicode.GeneralCategory.Ps = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.openPunctuation }

def Unicode.GeneralCategory.Pe : Unicode.GeneralCategory

General category: closing punctuation (Pe)

Equations

• Unicode.GeneralCategory.Pe = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.closePunctuation }

def Unicode.GeneralCategory.Pi : Unicode.GeneralCategory

General category: initial punctuation (Pi)

Equations

• Unicode.GeneralCategory.Pi = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.initialPunctuation }

def Unicode.GeneralCategory.Pf : Unicode.GeneralCategory

General category: final punctuation (Pf)

Equations

• Unicode.GeneralCategory.Pf = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.finalPunctuation }

def Unicode.GeneralCategory.Po : Unicode.GeneralCategory

General category: other punctuation (Po)

Equations

• Unicode.GeneralCategory.Po = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.otherPunctuation }

def Unicode.GeneralCategory.S : Unicode.GeneralCategory

General category: symbol (S)

Equations

• Unicode.GeneralCategory.S = { major := Unicode.MajorGeneralCategory.symbol, minor := none }

def Unicode.GeneralCategory.Sm : Unicode.GeneralCategory

General category: math symbol (Sm)

Equations

• Unicode.GeneralCategory.Sm = { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.mathSymbol }

def Unicode.GeneralCategory.Sc : Unicode.GeneralCategory

General category: currency symbol (Sc)

Equations

• Unicode.GeneralCategory.Sc = { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.currencySymbol }

def Unicode.GeneralCategory.Sk : Unicode.GeneralCategory

General category: modifier symbol (Sk)

Equations

• Unicode.GeneralCategory.Sk = { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.modifierSymbol }

def Unicode.GeneralCategory.So : Unicode.GeneralCategory

General category: other symbol (So)

Equations

• Unicode.GeneralCategory.So = { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.otherSymbol }

def Unicode.GeneralCategory.Z : Unicode.GeneralCategory

General category: separator (Z)

Equations

• Unicode.GeneralCategory.Z = { major := Unicode.MajorGeneralCategory.separator, minor := none }

def Unicode.GeneralCategory.Zs : Unicode.GeneralCategory

General category: space separator (Zs)

Equations

• Unicode.GeneralCategory.Zs = { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.spaceSeparator }

def Unicode.GeneralCategory.Zl : Unicode.GeneralCategory

General category: line separator (Zl)

Equations

• Unicode.GeneralCategory.Zl = { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.lineSeparator }

def Unicode.GeneralCategory.Zp : Unicode.GeneralCategory

General category: paragraph separator (Zp)

Equations

• Unicode.GeneralCategory.Zp = { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.paragraphSeparator }

def Unicode.GeneralCategory.C : Unicode.GeneralCategory

General category: other (C)

Equations

• Unicode.GeneralCategory.C = { major := Unicode.MajorGeneralCategory.other, minor := none }

def Unicode.GeneralCategory.Cc : Unicode.GeneralCategory

General category: control (Cc)

Equations

• Unicode.GeneralCategory.Cc = { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.control }

def Unicode.GeneralCategory.Cf : Unicode.GeneralCategory

General category: format (Cf)

Equations

• Unicode.GeneralCategory.Cf = { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.format }

def Unicode.GeneralCategory.Cs : Unicode.GeneralCategory

General category: surrogate (Cs)

Equations

• Unicode.GeneralCategory.Cs = { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.surrogate }

def Unicode.GeneralCategory.Co : Unicode.GeneralCategory

General category: private use (Co)

Equations

• Unicode.GeneralCategory.Co = { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.privateUse }

def Unicode.GeneralCategory.Cn : Unicode.GeneralCategory

General category: unassigned (Cn)

Equations

• Unicode.GeneralCategory.Cn = { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.unassigned }

def Unicode.GeneralCategory.toAbbrev : Unicode.GeneralCategory → String

String abbreviation for general category

Equations

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

def Unicode.GeneralCategory.ofAbbrev? (s : Substring) : Option Unicode.GeneralCategory

Get general category from string abbreviation

Equations

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

def Unicode.GeneralCategory.ofAbbrev! (s : Substring) : Unicode.GeneralCategory

Get general category from string abbreviation

Equations

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

instance Unicode.instReprGeneralCategory : Repr Unicode.GeneralCategory

Equations

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

Numeric Type and Value

inductive Unicode.NumericType : Type

Unicode numeric type

Unicode properties: Numeric_Type, Numeric_Value

• decimal: Fin 10 → Unicode.NumericType

  Decimal digit type and value

• digit: Fin 10 → Unicode.NumericType

  Digit type and value

• numeric: Int → Option Nat → Unicode.NumericType

  Numeric type and value

instance Unicode.instInhabitedNumericType : Inhabited Unicode.NumericType

Equations

• Unicode.instInhabitedNumericType = { default := Unicode.NumericType.decimal default }

instance Unicode.instDecidableEqNumericType : DecidableEq Unicode.NumericType

Equations

• Unicode.instDecidableEqNumericType = Unicode.decEqNumericType✝

instance Unicode.instReprNumericType : Repr Unicode.NumericType

Equations

• Unicode.instReprNumericType = { reprPrec := Unicode.reprNumericType✝ }

def Unicode.NumericType.isDecimal : Unicode.NumericType → Bool

Decimal digit type

The character is part of a sequence of contiguous code points representing decimal digits 0 through 9.

Unicode property: Numeric_Type

Equations

• x.isDecimal = match x with | Unicode.NumericType.decimal value => true | x => false

def Unicode.NumericType.isDigit : Unicode.NumericType → Bool

Digit type

The character represents a decimal digit 0 through 9.

Unicode property: Numeric_Type

Equations

• x.isDigit = match x with | Unicode.NumericType.decimal value => true | Unicode.NumericType.digit value => true | x => false

def Unicode.NumericType.value : Unicode.NumericType → Int ⊕ Int × Nat

Get the value of a numeric type

Returns either an integer value or a numerator-denominator pair representing a rational value.

Unicode property: Numeric_Value

Equations

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

Decomposition Mapping

inductive Unicode.CompatibilityTag : Type

Compatibility format tag

Unicode properties: Decomposition_Type, Decomposition_Mapping

• font: Unicode.CompatibilityTag

  Font variant

• noBreak: Unicode.CompatibilityTag

  No-break version of a space or hyphen

• initial: Unicode.CompatibilityTag

  Initial presentation form (Arabic)

• medial: Unicode.CompatibilityTag

  Medial presentation form (Arabic)

• final: Unicode.CompatibilityTag

  Final presentation form (Arabic)

• isolated: Unicode.CompatibilityTag

  Isolated presentation form (Arabic)

• circle: Unicode.CompatibilityTag

  Encircled form

• super: Unicode.CompatibilityTag

  Superscript form

• sub: Unicode.CompatibilityTag

  Subscript form

• vertical: Unicode.CompatibilityTag

  Vertical layout presentation form

• wide: Unicode.CompatibilityTag

  Wide (or zenkaku) compatibility character

• narrow: Unicode.CompatibilityTag

  Narrow (or hankaku) compatibility character

• small: Unicode.CompatibilityTag

  Small variant form (CNS compatibility)

• square: Unicode.CompatibilityTag

  CJK squared font variant

• fraction: Unicode.CompatibilityTag

  Vulgar fraction form

• compat: Unicode.CompatibilityTag

  Otherwise unspecified compatibility character

instance Unicode.instInhabitedCompatibilityTag : Inhabited Unicode.CompatibilityTag

Equations

• Unicode.instInhabitedCompatibilityTag = { default := Unicode.CompatibilityTag.font }

instance Unicode.instDecidableEqCompatibilityTag : DecidableEq Unicode.CompatibilityTag

Equations

• Unicode.instDecidableEqCompatibilityTag x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Unicode.instReprCompatibilityTag : Repr Unicode.CompatibilityTag

Equations

• Unicode.instReprCompatibilityTag = { reprPrec := Unicode.reprCompatibilityTag✝ }

instance Unicode.instToStringCompatibilityTag : ToString Unicode.CompatibilityTag

Equations

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

structure Unicode.DecompositionMapping : Type

Decomposition maping

Unicode properties: Decomposition_Type, Decomposition_Mapping

• tag : Option Unicode.CompatibilityTag

  Compatibility format tag

• mapping : List Char

  Decomposition mapping

instance Unicode.instInhabitedDecompositionMapping : Inhabited Unicode.DecompositionMapping

Equations

• Unicode.instInhabitedDecompositionMapping = { default := { tag := default, mapping := default } }

instance Unicode.instDecidableEqDecompositionMapping : DecidableEq Unicode.DecompositionMapping

Equations

• Unicode.instDecidableEqDecompositionMapping = Unicode.decEqDecompositionMapping✝

instance Unicode.instReprDecompositionMapping : Repr Unicode.DecompositionMapping

Equations

• Unicode.instReprDecompositionMapping = { reprPrec := Unicode.reprDecompositionMapping✝ }

Bidirectional Class

inductive Unicode.BidiClass : Type

Bidirectional class

Unicode property: Bidi_Class

• leftToRight: Unicode.BidiClass

  (L) strong left-to-right character

• rightToLeft: Unicode.BidiClass

  (R) strong right-to-left (non-Arabic-type) character

• arabicLetter: Unicode.BidiClass

  (AL) strong right-to-left (Arabic-type) character

• europeanNumber: Unicode.BidiClass

  (EN) ASCII digit or Eastern Arabic-Indic digit

• europeanSeparator: Unicode.BidiClass

  (ES) European separator: plus and

• europeanTerminator: Unicode.BidiClass

  (ET) European terminator in a numeric format context, includes currency signs

• arabicNumber: Unicode.BidiClass

  (AN) Arabic-Indic digit

• commonSeparator: Unicode.BidiClass

  (CS) common separator: commas, colons, and slashes

• nonspacingMark: Unicode.BidiClass

  (NSM) nonspacing mark

• boundaryNeutral: Unicode.BidiClass

  (BN) boundary neutral: most format characters, control codes, or noncharacters

• paragraphSeparator: Unicode.BidiClass

  (B) paragraph separator, various newline characters

• segmentSeparator: Unicode.BidiClass

  (S) segment separator, various segment-related control codes

• whiteSpace: Unicode.BidiClass

  (WS) white spaces

• otherNeutral: Unicode.BidiClass

  (ON) other neutral: most other symbols and punctuation marks

• leftToRightEmbedding: Unicode.BidiClass

  (LRE) left to right embedding (U+202A: the LR embedding control)

• leftToRightOverride: Unicode.BidiClass

  (LRO) Left_To_Right_Override (U+202D: the LR override control)

• rightToLeftEmbeding: Unicode.BidiClass

  (RLE) right-to-left embedding (U+202B: the RL embedding control)

• rightToLeftOverride: Unicode.BidiClass

  (RLO) right-to-left override (U+202E: the RL override control)

• popDirectionalFormat: Unicode.BidiClass

  (PDF) pop directional format (U+202C: terminates an embedding or override control)

• leftToRightIsolate: Unicode.BidiClass

  (LRI) left-to-right isolate (U+2066: the LR isolate control)

• rightToLeftIsolate: Unicode.BidiClass

  (RLI) right-toleft isolate (U+2067: the RL isolate control)

• firstStrongIsolate: Unicode.BidiClass

  (FSI) first strong isolate U+2068: the first strong isolate control

• popDirectionalIsolate: Unicode.BidiClass

  (PDI) pop directional isolate U+2069: terminates an isolate control

instance Unicode.instInhabitedBidiClass : Inhabited Unicode.BidiClass

Equations

• Unicode.instInhabitedBidiClass = { default := Unicode.BidiClass.leftToRight }

instance Unicode.instDecidableEqBidiClass : DecidableEq Unicode.BidiClass

Equations

• Unicode.instDecidableEqBidiClass x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Unicode.BidiClass.L : Unicode.BidiClass

Bidi class: strong left-to-right (L)

Equations

• Unicode.BidiClass.L = Unicode.BidiClass.leftToRight

def Unicode.BidiClass.R : Unicode.BidiClass

Bidi class: strong right-to-left (R)

Equations

• Unicode.BidiClass.R = Unicode.BidiClass.rightToLeft

def Unicode.BidiClass.AL : Unicode.BidiClass

Bidi class: arabic letter (AL)

Equations

• Unicode.BidiClass.AL = Unicode.BidiClass.arabicLetter

def Unicode.BidiClass.EN : Unicode.BidiClass

Bidi class: european number (EN)

Equations

• Unicode.BidiClass.EN = Unicode.BidiClass.europeanNumber

def Unicode.BidiClass.ES : Unicode.BidiClass

Bidi class: european separator (ES)

Equations

• Unicode.BidiClass.ES = Unicode.BidiClass.europeanSeparator

def Unicode.BidiClass.ET : Unicode.BidiClass

Bidi class: european terminator (ET)

Equations

• Unicode.BidiClass.ET = Unicode.BidiClass.europeanTerminator

def Unicode.BidiClass.AN : Unicode.BidiClass

Bidi class: arabic number (AN)

Equations

• Unicode.BidiClass.AN = Unicode.BidiClass.arabicNumber

def Unicode.BidiClass.CS : Unicode.BidiClass

Bidi class: common separator (CS)

Equations

• Unicode.BidiClass.CS = Unicode.BidiClass.commonSeparator

def Unicode.BidiClass.NSM : Unicode.BidiClass

Bidi class: nonspacing mark (NSM)

Equations

• Unicode.BidiClass.NSM = Unicode.BidiClass.nonspacingMark

def Unicode.BidiClass.BN : Unicode.BidiClass

Bidi class: boundary neutral (BN)

Equations

• Unicode.BidiClass.BN = Unicode.BidiClass.boundaryNeutral

def Unicode.BidiClass.B : Unicode.BidiClass

Bidi class: paragraph separator (B)

Equations

• Unicode.BidiClass.B = Unicode.BidiClass.paragraphSeparator

def Unicode.BidiClass.S : Unicode.BidiClass

Bidi class: segment separator (S)

Equations

• Unicode.BidiClass.S = Unicode.BidiClass.segmentSeparator

def Unicode.BidiClass.WS : Unicode.BidiClass

Bidi class: white space (WS)

Equations

• Unicode.BidiClass.WS = Unicode.BidiClass.whiteSpace

def Unicode.BidiClass.ON : Unicode.BidiClass

Bidi class: other neutral (ON)

Equations

• Unicode.BidiClass.ON = Unicode.BidiClass.otherNeutral

def Unicode.BidiClass.LRE : Unicode.BidiClass

Bidi class: left-to-right embedding (LRE)

Equations

• Unicode.BidiClass.LRE = Unicode.BidiClass.leftToRightEmbedding

def Unicode.BidiClass.LRO : Unicode.BidiClass

Bidi class: left-to-right override (LRO)

Equations

• Unicode.BidiClass.LRO = Unicode.BidiClass.leftToRightOverride

def Unicode.BidiClass.RLE : Unicode.BidiClass

Bidi class: right-to-left embedding (RLE)

Equations

• Unicode.BidiClass.RLE = Unicode.BidiClass.rightToLeftEmbeding

def Unicode.BidiClass.RLO : Unicode.BidiClass

Bidi class: right-to-left override (RLO)

Equations

• Unicode.BidiClass.RLO = Unicode.BidiClass.rightToLeftOverride

def Unicode.BidiClass.PDF : Unicode.BidiClass

Bidi class: pop directional format (PDF)

Equations

• Unicode.BidiClass.PDF = Unicode.BidiClass.popDirectionalFormat

def Unicode.BidiClass.LRI : Unicode.BidiClass

Bidi class: left-to-right isolate (LRI)

Equations

• Unicode.BidiClass.LRI = Unicode.BidiClass.leftToRightIsolate

def Unicode.BidiClass.RLI : Unicode.BidiClass

Bidi class: right-to-left isolate (RLI)

Equations

• Unicode.BidiClass.RLI = Unicode.BidiClass.rightToLeftIsolate

def Unicode.BidiClass.FSI : Unicode.BidiClass

Bidi class: first strong isolate (FSI)

Equations

• Unicode.BidiClass.FSI = Unicode.BidiClass.firstStrongIsolate

def Unicode.BidiClass.PDI : Unicode.BidiClass

Bidi class: pop directional isolate (PDI)

Equations

• Unicode.BidiClass.PDI = Unicode.BidiClass.popDirectionalIsolate

def Unicode.BidiClass.toAbbrev : Unicode.BidiClass → String

String abbreviation for bidi class

Equations

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

def Unicode.BidiClass.ofAbbrev? (abbr : Substring) : Option Unicode.BidiClass

Get bidi class from abbreviation

Equations

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

def Unicode.BidiClass.ofAbbrev! (abbr : Substring) : Unicode.BidiClass

Get bidi class from abbreviation

Equations

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

instance Unicode.instReprBidiClass : Repr Unicode.BidiClass

Equations

• Unicode.instReprBidiClass = { reprPrec := fun (bc : Unicode.BidiClass) (x : Nat) => Std.Format.text (toString "Unicode.BidiClass." ++ toString bc.toAbbrev ++ toString "") }

structure Unicode.UnicodeData : Type

Structure for data from UnicodeData.txt

• codeValue : UInt32

  Code Value

• characterName : Substring

  Character Name

• generalCategory : Unicode.GeneralCategory

  General Category

• canonicalCombiningClass : Nat

  Canonical Combining Class

• bidiClass : Unicode.BidiClass

  Bidirectional Class

• bidiMirrored : Bool

  Bidirectional Mirrored

• decompositionMapping : Option Unicode.DecompositionMapping

  Character Decomposition Mapping

• numeric : Option Unicode.NumericType

  Numeric Value

• uppercaseMapping : Option Char

  Uppercase Mapping

• lowercaseMapping : Option Char

  Lowercase Mapping

• titlecaseMapping : Option Char

  Titlecase Mapping

instance Unicode.instInhabitedUnicodeData : Inhabited Unicode.UnicodeData

Equations

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

instance Unicode.instBEqUnicodeData : BEq Unicode.UnicodeData

Equations

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

instance Unicode.instReprUnicodeData : Repr Unicode.UnicodeData

Equations

• Unicode.instReprUnicodeData = { reprPrec := Unicode.reprUnicodeData✝ }

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.