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 Batteries but not in Lean. It is scoped to Unicode here to avoid issues in low-level packages that don't use Batteries.

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 : MajorGeneralCategory

  (L) Letter

• mark : MajorGeneralCategory

  (M) Mark

• number : MajorGeneralCategory

  (N) Number

• punctuation : MajorGeneralCategory

  (P) Punctuation

• symbol : MajorGeneralCategory

  (S) Symbol

• separator : MajorGeneralCategory

  (Z) Separator

• other : MajorGeneralCategory

  (C) Other

instance Unicode.instInhabitedMajorGeneralCategory : Inhabited MajorGeneralCategory

Equations

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

instance Unicode.instDecidableEqMajorGeneralCategory : DecidableEq MajorGeneralCategory

Equations

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

def Unicode.MajorGeneralCategory.toAbbrev : MajorGeneralCategory → String

String abbreviation for major general category

Equations

• Unicode.MajorGeneralCategory.letter.toAbbrev = "L"
• Unicode.MajorGeneralCategory.mark.toAbbrev = "M"
• Unicode.MajorGeneralCategory.number.toAbbrev = "N"
• Unicode.MajorGeneralCategory.punctuation.toAbbrev = "P"
• Unicode.MajorGeneralCategory.symbol.toAbbrev = "S"
• Unicode.MajorGeneralCategory.separator.toAbbrev = "Z"
• Unicode.MajorGeneralCategory.other.toAbbrev = "C"

inductive Unicode.MinorGeneralCategory : MajorGeneralCategory → Type

Minor general category

Unicode property: General_Category

• casedLetter : MinorGeneralCategory MajorGeneralCategory.letter

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

• uppercaseLetter : MinorGeneralCategory MajorGeneralCategory.letter

  (Lu) uppercase letter

• lowercaseLetter : MinorGeneralCategory MajorGeneralCategory.letter

  (Ll) lowercase letter

• titlecaseLetter : MinorGeneralCategory MajorGeneralCategory.letter

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

• modifierLetter : MinorGeneralCategory MajorGeneralCategory.letter

  (Lm) modifier letter

• otherLetter : MinorGeneralCategory MajorGeneralCategory.letter

  (Lo) other letters, including syllables and ideographs

• nonspacingMark : MinorGeneralCategory MajorGeneralCategory.mark

  (Mn) nonspacing combining mark (zero advance width)

• spacingMark : MinorGeneralCategory MajorGeneralCategory.mark

  (Mc) spacing combining mark (positive advance width)

• enclosingMark : MinorGeneralCategory MajorGeneralCategory.mark

  (Me) enclosing combining mark

• decimalNumber : MinorGeneralCategory MajorGeneralCategory.number

  (Nd) decimal digit

• letterNumber : MinorGeneralCategory MajorGeneralCategory.number

  (Nl) letter number: a letterlike numeric character

• otherNumber : MinorGeneralCategory MajorGeneralCategory.number

  (No) numeric character of other type

• connectorPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Pc) connecting punctuation mark, like a tie

• dashPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Pd) dash or hyphen punctuation mark

• groupPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (PG) grouping punctuation mark (derived from Ps | Pe)

• openPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Ps) opening punctuation mark (of a pair)

• closePunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Pe) closing punctuation mark (of a pair)

• quotePunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (PQ) quoting punctuation mark (derived from Pi | Pf)

• initialPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Pi) initial quotation mark

• finalPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Pf) final quotation mark

• otherPunctuation : MinorGeneralCategory MajorGeneralCategory.punctuation

  (Po) punctuation mark of other type

• mathSymbol : MinorGeneralCategory MajorGeneralCategory.symbol

  (Sm) symbol of mathematical use

• currencySymbol : MinorGeneralCategory MajorGeneralCategory.symbol

  (Sc) currency sign

• modifierSymbol : MinorGeneralCategory MajorGeneralCategory.symbol

  (Sk) non-letterlike modifier symbol

• otherSymbol : MinorGeneralCategory MajorGeneralCategory.symbol

  (So) symbol of other type

• spaceSeparator : MinorGeneralCategory MajorGeneralCategory.separator

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

• lineSeparator : MinorGeneralCategory MajorGeneralCategory.separator

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

• paragraphSeparator : MinorGeneralCategory MajorGeneralCategory.separator

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

• control : MinorGeneralCategory MajorGeneralCategory.other

  (Cc) C0 or C1 control code

• format : MinorGeneralCategory MajorGeneralCategory.other

  (Cf) format control character

• surrogate : MinorGeneralCategory MajorGeneralCategory.other

  (Cs) surrogate code point

• privateUse : MinorGeneralCategory MajorGeneralCategory.other

  (Co) private-use character

• unassigned : MinorGeneralCategory MajorGeneralCategory.other

  (Cn) reserved unassigned code point or a noncharacter

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

Equations

• Unicode.instDecidableEqMinorGeneralCategory = Unicode.decEqMinorGeneralCategory✝

structure Unicode.GeneralCategory : Type

General category of a code point

Unicode property: General_Category

• major : MajorGeneralCategory

  Major general category of a code point

• minor : Option (MinorGeneralCategory self.major)

  Minor general category of a code point

instance Unicode.instInhabitedGeneralCategory : Inhabited GeneralCategory

Equations

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

instance Unicode.instDecidableEqGeneralCategory : DecidableEq GeneralCategory

Equations

• Unicode.instDecidableEqGeneralCategory = Unicode.decEqGeneralCategory✝

def Unicode.GeneralCategory.L : GeneralCategory

General category: letter (L)

Equations

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

def Unicode.GeneralCategory.LC : GeneralCategory

General category: cased letter (LC)

Equations

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

def Unicode.GeneralCategory.Lu : GeneralCategory

General category: uppercase letter (Lu)

Equations

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

def Unicode.GeneralCategory.Ll : GeneralCategory

General category: lowercase letter (Ll)

Equations

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

def Unicode.GeneralCategory.Lt : GeneralCategory

General category: titlecase letter (Lt)

Equations

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

def Unicode.GeneralCategory.Lm : GeneralCategory

General category: modifier letter (Lm)

Equations

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

def Unicode.GeneralCategory.Lo : GeneralCategory

General category: other letter (Lo)

Equations

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

def Unicode.GeneralCategory.M : GeneralCategory

General category mark (M)

Equations

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

def Unicode.GeneralCategory.Mn : GeneralCategory

General category: nonspacing combining mark (Mn)

Equations

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

def Unicode.GeneralCategory.Mc : GeneralCategory

General category: spacing combining mark (Mc)

Equations

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

def Unicode.GeneralCategory.Me : GeneralCategory

General category: enclosing combining mark (Me)

Equations

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

def Unicode.GeneralCategory.N : GeneralCategory

General category: number (N)

Equations

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

def Unicode.GeneralCategory.Nd : GeneralCategory

General category: decimal digit (Nd)

Equations

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

def Unicode.GeneralCategory.Nl : GeneralCategory

General category: letter number (Nl)

Equations

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

def Unicode.GeneralCategory.No : GeneralCategory

General category: other number (No)

Equations

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

def Unicode.GeneralCategory.P : GeneralCategory

General category: punctuation (P)

Equations

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

def Unicode.GeneralCategory.Pc : GeneralCategory

General category: connector punctuation (Pc)

Equations

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

def Unicode.GeneralCategory.Pd : GeneralCategory

General category: dash punctuation (Pd)

Equations

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

def Unicode.GeneralCategory.PG : GeneralCategory

General category: grouping punctuation (PG)

Equations

• Unicode.GeneralCategory.PG = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.groupPunctuation }

def Unicode.GeneralCategory.Ps : GeneralCategory

General category: opening punctuation (Ps)

Equations

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

def Unicode.GeneralCategory.Pe : GeneralCategory

General category: closing punctuation (Pe)

Equations

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

def Unicode.GeneralCategory.PQ : GeneralCategory

General category: quoting punctuation (PQ)

Equations

• Unicode.GeneralCategory.PQ = { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.quotePunctuation }

def Unicode.GeneralCategory.Pi : GeneralCategory

General category: initial punctuation (Pi)

Equations

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

def Unicode.GeneralCategory.Pf : GeneralCategory

General category: final punctuation (Pf)

Equations

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

def Unicode.GeneralCategory.Po : GeneralCategory

General category: other punctuation (Po)

Equations

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

def Unicode.GeneralCategory.S : GeneralCategory

General category: symbol (S)

Equations

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

def Unicode.GeneralCategory.Sm : GeneralCategory

General category: math symbol (Sm)

Equations

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

def Unicode.GeneralCategory.Sc : GeneralCategory

General category: currency symbol (Sc)

Equations

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

def Unicode.GeneralCategory.Sk : GeneralCategory

General category: modifier symbol (Sk)

Equations

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

def Unicode.GeneralCategory.So : GeneralCategory

General category: other symbol (So)

Equations

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

def Unicode.GeneralCategory.Z : GeneralCategory

General category: separator (Z)

Equations

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

def Unicode.GeneralCategory.Zs : GeneralCategory

General category: space separator (Zs)

Equations

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

def Unicode.GeneralCategory.Zl : GeneralCategory

General category: line separator (Zl)

Equations

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

def Unicode.GeneralCategory.Zp : GeneralCategory

General category: paragraph separator (Zp)

Equations

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

def Unicode.GeneralCategory.C : GeneralCategory

General category: other (C)

Equations

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

def Unicode.GeneralCategory.Cc : GeneralCategory

General category: control (Cc)

Equations

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

def Unicode.GeneralCategory.Cf : GeneralCategory

General category: format (Cf)

Equations

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

def Unicode.GeneralCategory.Cs : GeneralCategory

General category: surrogate (Cs)

Equations

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

def Unicode.GeneralCategory.Co : GeneralCategory

General category: private use (Co)

Equations

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

def Unicode.GeneralCategory.Cn : GeneralCategory

General category: unassigned (Cn)

Equations

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

def Unicode.GeneralCategory.toAbbrev : GeneralCategory → String

String abbreviation for general category

def Unicode.GeneralCategory.ofAbbrev? (s : Substring) : Option 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) : GeneralCategory

Get general category from string abbreviation

Equations

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

instance Unicode.instReprGeneralCategory : Repr 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 (value : Fin 10) : NumericType

  Decimal digit type and value

• digit (value : Fin 10) : NumericType

  Digit type and value

• numeric (num : Int) (den : Option Nat) : NumericType

  Numeric type and value

instance Unicode.instInhabitedNumericType : Inhabited NumericType

Equations

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

instance Unicode.instDecidableEqNumericType : DecidableEq NumericType

Equations

• Unicode.instDecidableEqNumericType = Unicode.decEqNumericType✝

instance Unicode.instReprNumericType : Repr NumericType

Equations

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

def Unicode.NumericType.isDecimal : 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

• (Unicode.NumericType.decimal value).isDecimal = true
• x✝.isDecimal = false

def Unicode.NumericType.isDigit : NumericType → Bool

Digit type

The character represents a decimal digit 0 through 9.

Unicode property: Numeric_Type

Equations

• (Unicode.NumericType.decimal value).isDigit = true
• (Unicode.NumericType.digit value).isDigit = true
• x✝.isDigit = false

def Unicode.NumericType.value : 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

• (Unicode.NumericType.decimal n).value = Sum.inl ↑↑n
• (Unicode.NumericType.digit n).value = Sum.inl ↑↑n
• (Unicode.NumericType.numeric n none).value = Sum.inl n
• (Unicode.NumericType.numeric n (some d)).value = Sum.inr (n, d)

Decomposition Mapping

inductive Unicode.CompatibilityTag : Type

Compatibility format tag

Unicode properties: Decomposition_Type, Decomposition_Mapping

• font : CompatibilityTag

  Font variant

• noBreak : CompatibilityTag

  No-break version of a space or hyphen

• initial : CompatibilityTag

  Initial presentation form (Arabic)

• medial : CompatibilityTag

  Medial presentation form (Arabic)

• final : CompatibilityTag

  Final presentation form (Arabic)

• isolated : CompatibilityTag

  Isolated presentation form (Arabic)

• circle : CompatibilityTag

  Encircled form

• super : CompatibilityTag

  Superscript form

• sub : CompatibilityTag

  Subscript form

• vertical : CompatibilityTag

  Vertical layout presentation form

• wide : CompatibilityTag

  Wide (or zenkaku) compatibility character

• narrow : CompatibilityTag

  Narrow (or hankaku) compatibility character

• small : CompatibilityTag

  Small variant form (CNS compatibility)

• square : CompatibilityTag

  CJK squared font variant

• fraction : CompatibilityTag

  Vulgar fraction form

• compat : CompatibilityTag

  Otherwise unspecified compatibility character

instance Unicode.instInhabitedCompatibilityTag : Inhabited CompatibilityTag

Equations

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

instance Unicode.instDecidableEqCompatibilityTag : DecidableEq CompatibilityTag

Equations

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

instance Unicode.instReprCompatibilityTag : Repr CompatibilityTag

Equations

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

instance Unicode.instToStringCompatibilityTag : ToString 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 CompatibilityTag

  Compatibility format tag

• mapping : List Char

  Decomposition mapping

instance Unicode.instInhabitedDecompositionMapping : Inhabited DecompositionMapping

Equations

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

instance Unicode.instDecidableEqDecompositionMapping : DecidableEq DecompositionMapping

Equations

• Unicode.instDecidableEqDecompositionMapping = Unicode.decEqDecompositionMapping✝

instance Unicode.instReprDecompositionMapping : Repr DecompositionMapping

Equations

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

Bidirectional Class

inductive Unicode.BidiClass : Type

Bidirectional class

Unicode property: Bidi_Class

• leftToRight : BidiClass

  (L) strong left-to-right character

• rightToLeft : BidiClass

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

• arabicLetter : BidiClass

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

• europeanNumber : BidiClass

  (EN) ASCII digit or Eastern Arabic-Indic digit

• europeanSeparator : BidiClass

  (ES) European separator: plus and

• europeanTerminator : BidiClass

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

• arabicNumber : BidiClass

  (AN) Arabic-Indic digit

• commonSeparator : BidiClass

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

• nonspacingMark : BidiClass

  (NSM) nonspacing mark

• boundaryNeutral : BidiClass

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

• paragraphSeparator : BidiClass

  (B) paragraph separator, various newline characters

• segmentSeparator : BidiClass

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

• whiteSpace : BidiClass

  (WS) white spaces

• otherNeutral : BidiClass

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

• leftToRightEmbedding : BidiClass

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

• leftToRightOverride : BidiClass

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

• rightToLeftEmbeding : BidiClass

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

• rightToLeftOverride : BidiClass

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

• popDirectionalFormat : BidiClass

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

• leftToRightIsolate : BidiClass

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

• rightToLeftIsolate : BidiClass

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

• firstStrongIsolate : BidiClass

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

• popDirectionalIsolate : BidiClass

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

instance Unicode.instInhabitedBidiClass : Inhabited BidiClass

Equations

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

instance Unicode.instDecidableEqBidiClass : DecidableEq BidiClass

Equations

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

def Unicode.BidiClass.L : BidiClass

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

Equations

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

def Unicode.BidiClass.R : BidiClass

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

Equations

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

def Unicode.BidiClass.AL : BidiClass

Bidi class: arabic letter (AL)

Equations

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

def Unicode.BidiClass.EN : BidiClass

Bidi class: european number (EN)

Equations

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

def Unicode.BidiClass.ES : BidiClass

Bidi class: european separator (ES)

Equations

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

def Unicode.BidiClass.ET : BidiClass

Bidi class: european terminator (ET)

Equations

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

def Unicode.BidiClass.AN : BidiClass

Bidi class: arabic number (AN)

Equations

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

def Unicode.BidiClass.CS : BidiClass

Bidi class: common separator (CS)

Equations

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

def Unicode.BidiClass.NSM : BidiClass

Bidi class: nonspacing mark (NSM)

Equations

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

def Unicode.BidiClass.BN : BidiClass

Bidi class: boundary neutral (BN)

Equations

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

def Unicode.BidiClass.B : BidiClass

Bidi class: paragraph separator (B)

Equations

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

def Unicode.BidiClass.S : BidiClass

Bidi class: segment separator (S)

Equations

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

def Unicode.BidiClass.WS : BidiClass

Bidi class: white space (WS)

Equations

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

def Unicode.BidiClass.ON : BidiClass

Bidi class: other neutral (ON)

Equations

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

def Unicode.BidiClass.LRE : BidiClass

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

Equations

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

def Unicode.BidiClass.LRO : BidiClass

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

Equations

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

def Unicode.BidiClass.RLE : BidiClass

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

Equations

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

def Unicode.BidiClass.RLO : BidiClass

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

Equations

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

def Unicode.BidiClass.PDF : BidiClass

Bidi class: pop directional format (PDF)

Equations

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

def Unicode.BidiClass.LRI : BidiClass

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

Equations

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

def Unicode.BidiClass.RLI : BidiClass

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

Equations

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

def Unicode.BidiClass.FSI : BidiClass

Bidi class: first strong isolate (FSI)

Equations

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

def Unicode.BidiClass.PDI : BidiClass

Bidi class: pop directional isolate (PDI)

Equations

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

def Unicode.BidiClass.toAbbrev : BidiClass → String

String abbreviation for bidi class

Equations

• Unicode.BidiClass.leftToRight.toAbbrev = "L"
• Unicode.BidiClass.rightToLeft.toAbbrev = "R"
• Unicode.BidiClass.arabicLetter.toAbbrev = "AL"
• Unicode.BidiClass.europeanNumber.toAbbrev = "EN"
• Unicode.BidiClass.europeanSeparator.toAbbrev = "ES"
• Unicode.BidiClass.europeanTerminator.toAbbrev = "ET"
• Unicode.BidiClass.arabicNumber.toAbbrev = "AN"
• Unicode.BidiClass.commonSeparator.toAbbrev = "CS"
• Unicode.BidiClass.nonspacingMark.toAbbrev = "NSM"
• Unicode.BidiClass.boundaryNeutral.toAbbrev = "BN"
• Unicode.BidiClass.paragraphSeparator.toAbbrev = "B"
• Unicode.BidiClass.segmentSeparator.toAbbrev = "S"
• Unicode.BidiClass.whiteSpace.toAbbrev = "WS"
• Unicode.BidiClass.otherNeutral.toAbbrev = "ON"
• Unicode.BidiClass.leftToRightEmbedding.toAbbrev = "LRE"
• Unicode.BidiClass.leftToRightOverride.toAbbrev = "LRO"
• Unicode.BidiClass.rightToLeftEmbeding.toAbbrev = "RLE"
• Unicode.BidiClass.rightToLeftOverride.toAbbrev = "RLO"
• Unicode.BidiClass.popDirectionalFormat.toAbbrev = "PDF"
• Unicode.BidiClass.leftToRightIsolate.toAbbrev = "LRI"
• Unicode.BidiClass.rightToLeftIsolate.toAbbrev = "RLI"
• Unicode.BidiClass.firstStrongIsolate.toAbbrev = "FSI"
• Unicode.BidiClass.popDirectionalIsolate.toAbbrev = "PDI"

def Unicode.BidiClass.ofAbbrev? (abbr : Substring) : Option 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) : BidiClass

Get bidi class from abbreviation

Equations

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

instance Unicode.instReprBidiClass : Repr 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 : GeneralCategory

  General Category

• canonicalCombiningClass : Nat

  Canonical Combining Class

• bidiClass : BidiClass

  Bidirectional Class

• bidiMirrored : Bool

  Bidirectional Mirrored

• decompositionMapping : Option DecompositionMapping

  Character Decomposition Mapping

• numeric : Option NumericType

  Numeric Value

• uppercaseMapping : Option Char

  Uppercase Mapping

• lowercaseMapping : Option Char

  Lowercase Mapping

• titlecaseMapping : Option Char

  Titlecase Mapping

instance Unicode.instBEqUnicodeData : BEq UnicodeData

Equations

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

instance Unicode.instReprUnicodeData : Repr UnicodeData

Equations

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

instance Unicode.instInhabitedUnicodeData : Inhabited UnicodeData

Equations

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