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

@[reducible, inline]

abbrev Unicode.max : UInt32

Maximum valid code point value

Equations

• Unicode.max = 1114111

@[reducible, inline]

abbrev Unicode.minHighSurrogate : UInt32

Minimum high surrogate code point

Equations

• Unicode.minHighSurrogate = 55296

@[reducible, inline]

abbrev Unicode.maxHighSurrogate : UInt32

Maximum high surrogate code point

Equations

• Unicode.maxHighSurrogate = 56319

@[reducible, inline]

abbrev Unicode.minLowSurrogate : UInt32

Minimum low surrogate code point

Equations

• Unicode.minLowSurrogate = 56320

@[reducible, inline]

abbrev Unicode.maxLowSurrogate : UInt32

Maximum low surrogate code point

Equations

• Unicode.maxLowSurrogate = 57343

@[reducible, inline]

abbrev Unicode.minSurrogate : UInt32

Minimum surrogate code point

Equations

• Unicode.minSurrogate = Unicode.minHighSurrogate

@[reducible, inline]

abbrev Unicode.maxSurrogate : UInt32

Maximum surrogate code point

Equations

• Unicode.maxSurrogate = Unicode.maxLowSurrogate

def Unicode.toHexStringRaw (code : UInt32) : String

Raw 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.toHexStringRaw code

def Unicode.ofHexString? (str : String.Slice) : 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.

def Unicode.ofHexString! (str : String.Slice) : 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

def Unicode.GC : Type

General category (GC)

A value of this type is a set of general categories. Derived categories (such as GC.L) are unions of basic categories (such as GC.Lu), GC.none is the empty set and GC.univ is the set of all categories.

Unicode property: General_Category

Equations

• Unicode.GC = UInt32

@[instance_reducible]

instance Unicode.instDecidableEqGC : DecidableEq GC

Equations

• Unicode.instDecidableEqGC = Unicode.instDecidableEqGC._aux_1

@[instance_reducible]

instance Unicode.instInhabitedGC : Inhabited GC

Equations

• Unicode.instInhabitedGC = { default := Unicode.instInhabitedGC._aux_1 }

@[instance_reducible]

instance Unicode.GC.instOrOp : OrOp GC

Equations

• Unicode.GC.instOrOp = { or := Unicode.GC.instOrOp._aux_1 }

@[instance_reducible]

instance Unicode.GC.instAndOp : AndOp GC

Equations

• Unicode.GC.instAndOp = { and := Unicode.GC.instAndOp._aux_1 }

@[instance_reducible]

instance Unicode.GC.instComplement : Complement GC

Equations

• Unicode.GC.instComplement = { complement := fun (x : Unicode.GC) => UInt32.xor x 1073741823 }

@[instance_reducible]

instance Unicode.GC.instHasSubset : HasSubset GC

Equations

• Unicode.GC.instHasSubset = { Subset := fun (x y : Unicode.GC) => (x &&& y == x) = true }

@[instance_reducible]

instance Unicode.GC.instDecidableSubset (x y : GC) : Decidable (x ⊆ y)

Equations

• x.instDecidableSubset y = instDecidableEqBool (x &&& y == x) true

@[reducible, inline]

abbrev Unicode.GC.none : GC

Equations

• Unicode.GC.none = 0

@[reducible, inline]

abbrev Unicode.GC.univ : GC

Equations

• Unicode.GC.univ = 1073741823

@[reducible, inline]

abbrev Unicode.GC.Lu : GC

Equations

• Unicode.GC.Lu = 1

@[reducible, inline]

abbrev Unicode.GC.Ll : GC

Equations

• Unicode.GC.Ll = 2

@[reducible, inline]

abbrev Unicode.GC.Lt : GC

Equations

• Unicode.GC.Lt = 4

@[reducible, inline]

abbrev Unicode.GC.Lm : GC

Equations

• Unicode.GC.Lm = 8

@[reducible, inline]

abbrev Unicode.GC.Lo : GC

Equations

• Unicode.GC.Lo = 16

@[reducible, inline]

abbrev Unicode.GC.LC : GC

Equations

• Unicode.GC.LC = Unicode.GC.Lu ||| Unicode.GC.Ll ||| Unicode.GC.Lt

@[reducible, inline]

abbrev Unicode.GC.L : GC

Equations

• Unicode.GC.L = Unicode.GC.Lu ||| Unicode.GC.Ll ||| Unicode.GC.Lt ||| Unicode.GC.Lm ||| Unicode.GC.Lo

@[reducible, inline]

abbrev Unicode.GC.Mn : GC

Equations

• Unicode.GC.Mn = 32

@[reducible, inline]

abbrev Unicode.GC.Mc : GC

Equations

• Unicode.GC.Mc = 64

@[reducible, inline]

abbrev Unicode.GC.Me : GC

Equations

• Unicode.GC.Me = 128

@[reducible, inline]

abbrev Unicode.GC.M : GC

Equations

• Unicode.GC.M = Unicode.GC.Mn ||| Unicode.GC.Mc ||| Unicode.GC.Me

@[reducible, inline]

abbrev Unicode.GC.Nd : GC

Equations

• Unicode.GC.Nd = 256

@[reducible, inline]

abbrev Unicode.GC.Nl : GC

Equations

• Unicode.GC.Nl = 512

@[reducible, inline]

abbrev Unicode.GC.No : GC

Equations

• Unicode.GC.No = 1024

@[reducible, inline]

abbrev Unicode.GC.N : GC

Equations

• Unicode.GC.N = Unicode.GC.Nd ||| Unicode.GC.Nl ||| Unicode.GC.No

@[reducible, inline]

abbrev Unicode.GC.Pc : GC

Equations

• Unicode.GC.Pc = 2048

@[reducible, inline]

abbrev Unicode.GC.Pd : GC

Equations

• Unicode.GC.Pd = 4096

@[reducible, inline]

abbrev Unicode.GC.Ps : GC

Equations

• Unicode.GC.Ps = 8192

@[reducible, inline]

abbrev Unicode.GC.Pe : GC

Equations

• Unicode.GC.Pe = 16384

@[reducible, inline]

abbrev Unicode.GC.Pi : GC

Equations

• Unicode.GC.Pi = 32768

@[reducible, inline]

abbrev Unicode.GC.Pf : GC

Equations

• Unicode.GC.Pf = 65536

@[reducible, inline]

abbrev Unicode.GC.Po : GC

Equations

• Unicode.GC.Po = 131072

@[reducible, inline]

abbrev Unicode.GC.PG : GC

Equations

• Unicode.GC.PG = Unicode.GC.Ps ||| Unicode.GC.Pe

@[reducible, inline]

abbrev Unicode.GC.PQ : GC

Equations

• Unicode.GC.PQ = Unicode.GC.Pi ||| Unicode.GC.Pf

@[reducible, inline]

abbrev Unicode.GC.P : GC

Equations

• Unicode.GC.P = Unicode.GC.Pc ||| Unicode.GC.Pd ||| Unicode.GC.Ps ||| Unicode.GC.Pe ||| Unicode.GC.Pi ||| Unicode.GC.Pf ||| Unicode.GC.Po

@[reducible, inline]

abbrev Unicode.GC.Sm : GC

Equations

• Unicode.GC.Sm = 262144

@[reducible, inline]

abbrev Unicode.GC.Sc : GC

Equations

• Unicode.GC.Sc = 524288

@[reducible, inline]

abbrev Unicode.GC.Sk : GC

Equations

• Unicode.GC.Sk = 1048576

@[reducible, inline]

abbrev Unicode.GC.So : GC

Equations

• Unicode.GC.So = 2097152

@[reducible, inline]

abbrev Unicode.GC.S : GC

Equations

• Unicode.GC.S = Unicode.GC.Sm ||| Unicode.GC.Sc ||| Unicode.GC.Sk ||| Unicode.GC.So

@[reducible, inline]

abbrev Unicode.GC.Zs : GC

Equations

• Unicode.GC.Zs = 4194304

@[reducible, inline]

abbrev Unicode.GC.Zl : GC

Equations

• Unicode.GC.Zl = 8388608

@[reducible, inline]

abbrev Unicode.GC.Zp : GC

Equations

• Unicode.GC.Zp = 16777216

@[reducible, inline]

abbrev Unicode.GC.Z : GC

Equations

• Unicode.GC.Z = Unicode.GC.Zs ||| Unicode.GC.Zl ||| Unicode.GC.Zp

@[reducible, inline]

abbrev Unicode.GC.Cc : GC

Equations

• Unicode.GC.Cc = 33554432

@[reducible, inline]

abbrev Unicode.GC.Cf : GC

Equations

• Unicode.GC.Cf = 67108864

@[reducible, inline]

abbrev Unicode.GC.Cs : GC

Equations

• Unicode.GC.Cs = 134217728

@[reducible, inline]

abbrev Unicode.GC.Co : GC

Equations

• Unicode.GC.Co = 268435456

@[reducible, inline]

abbrev Unicode.GC.Cn : GC

Equations

• Unicode.GC.Cn = 536870912

@[reducible, inline]

abbrev Unicode.GC.C : GC

Equations

• Unicode.GC.C = Unicode.GC.Cc ||| Unicode.GC.Cf ||| Unicode.GC.Cs ||| Unicode.GC.Co ||| Unicode.GC.Cn

@[inline]

def Unicode.GC.toAbbrev! (x : GC) : String

Equations

• x.toAbbrev! = match Unicode.GC.reprAux✝ x true with | [a] => a | x => panicWithPosWithDecl "UnicodeBasic.Types" "Unicode.GC.toAbbrev!" 280 9 "invalid general category"

def Unicode.GC.reprPrec (x : GC) (prec : Nat) : Std.Format

Equations

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

@[instance_reducible]

instance Unicode.GC.instRepr : Repr GC

Equations

• Unicode.GC.instRepr = { reprPrec := Unicode.GC.reprPrec }

def Unicode.GC.toString (x : GC) : String

Equations

• x.toString = " | ".intercalate (Unicode.GC.reprAux✝ x)

@[instance_reducible]

instance Unicode.GC.instToString : ToString GC

Equations

• Unicode.GC.instToString = { toString := Unicode.GC.toString }

def Unicode.GC.ofAbbrev? (s : String.Slice) : Option GC

Equations

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

def Unicode.GC.ofAbbrev! (s : String.Slice) : GC

Equations

• Unicode.GC.ofAbbrev! s = match Unicode.GC.ofAbbrev? s with | some c => c | none => panicWithPosWithDecl "UnicodeBasic.Types" "Unicode.GC.ofAbbrev!" 336 12 "invalid general category"

def Unicode.GC.ofString? (s : String.Slice) : Option GC

Equations

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

def Unicode.GC.ofString! (s : String.Slice) : GC

Equations

• Unicode.GC.ofString! s = match Unicode.GC.ofString? s with | some c => c | none => panicWithPosWithDecl "UnicodeBasic.Types" "Unicode.GC.ofString!" 347 12 "invalid general category"

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_reducible]

instance Unicode.instInhabitedNumericType : Inhabited NumericType

Equations

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

def Unicode.instDecidableEqNumericType.decEq (x✝ x✝¹ : NumericType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.decimal a) (Unicode.NumericType.decimal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.decimal value) (Unicode.NumericType.digit value_1) = isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.decimal value) (Unicode.NumericType.numeric num den) = isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.digit value) (Unicode.NumericType.decimal value_1) = isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.digit a) (Unicode.NumericType.digit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.digit value) (Unicode.NumericType.numeric num den) = isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.numeric num den) (Unicode.NumericType.decimal value) = isFalse ⋯
• Unicode.instDecidableEqNumericType.decEq (Unicode.NumericType.numeric num den) (Unicode.NumericType.digit value) = isFalse ⋯

@[instance_reducible]

instance Unicode.instDecidableEqNumericType : DecidableEq NumericType

Equations

• Unicode.instDecidableEqNumericType = Unicode.instDecidableEqNumericType.decEq

@[instance_reducible]

instance Unicode.instReprNumericType : Repr NumericType

Equations

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

def Unicode.instReprNumericType.repr : NumericType → Nat → Std.Format

Equations

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

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_reducible]

instance Unicode.instInhabitedCompatibilityTag : Inhabited CompatibilityTag

Equations

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

@[instance_reducible]

instance Unicode.instDecidableEqCompatibilityTag : DecidableEq CompatibilityTag

Equations

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

def Unicode.instReprCompatibilityTag.repr : CompatibilityTag → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Unicode.instReprCompatibilityTag : Repr CompatibilityTag

Equations

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

@[instance_reducible]

instance Unicode.instToStringCompatibilityTag : ToString CompatibilityTag

Equations

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

structure Unicode.DecompositionMapping : Type

Decomposition mapping

Unicode properties: Decomposition_Type, Decomposition_Mapping

• tag : Option CompatibilityTag

  Compatibility format tag

• mapping : List Char

  Decomposition mapping

@[instance_reducible]

instance Unicode.instInhabitedDecompositionMapping : Inhabited DecompositionMapping

Equations

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

def Unicode.instDecidableEqDecompositionMapping.decEq (x✝ x✝¹ : DecompositionMapping) : Decidable (x✝ = x✝¹)

Equations

• Unicode.instDecidableEqDecompositionMapping.decEq { tag := a, mapping := a_1 } { tag := b, mapping := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Unicode.instDecidableEqDecompositionMapping : DecidableEq DecompositionMapping

Equations

• Unicode.instDecidableEqDecompositionMapping = Unicode.instDecidableEqDecompositionMapping.decEq

@[instance_reducible]

instance Unicode.instReprDecompositionMapping : Repr DecompositionMapping

Equations

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

def Unicode.instReprDecompositionMapping.repr : DecompositionMapping → Nat → Std.Format

Equations

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

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 minus signs

• 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)

• rightToLeftEmbedding : 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-to-left 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_reducible]

instance Unicode.instInhabitedBidiClass : Inhabited BidiClass

Equations

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

@[instance_reducible]

instance Unicode.instDecidableEqBidiClass : DecidableEq BidiClass

Equations

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

@[reducible, match_pattern, inline, deprecated Unicode.BidiClass.rightToLeftEmbedding (since := "2026-10-06")]

abbrev Unicode.BidiClass.rightToLeftEmbeding : BidiClass

Equations

• Unicode.BidiClass.rightToLeftEmbeding = Unicode.BidiClass.rightToLeftEmbedding

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.rightToLeftEmbedding

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.rightToLeftEmbedding.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 : String.Slice) : 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 : String.Slice) : BidiClass

Get bidi class from abbreviation

Equations

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

@[instance_reducible]

instance Unicode.instReprBidiClass : Repr BidiClass

Equations

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

Scripts

@[inline]

def Unicode.Script.isValid (c : UInt32) : Bool

Check if valid script identifier

A valid script identifier consists of an uppercase letter followed by three lowercase letters.

Equations

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

structure Unicode.Script : Type

Script identifier type

A script is identified by its four-letter ISO 15924 code, such as Latn for Latin. Use Script.ofAbbrev? and Script.toAbbrev to convert from and to this code.

• code : UInt32
• is_valid : isValid self.code = true

@[instance_reducible]

instance Unicode.instDecidableEqScript : DecidableEq Script

Equations

• Unicode.instDecidableEqScript = Unicode.instDecidableEqScript.decEq

def Unicode.instDecidableEqScript.decEq (x✝ x✝¹ : Script) : Decidable (x✝ = x✝¹)

Equations

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

def Unicode.instHashableScript.hash : Script → UInt64

Equations

• Unicode.instHashableScript.hash { code := a, is_valid := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance Unicode.instHashableScript : Hashable Script

Equations

• Unicode.instHashableScript = { hash := Unicode.instHashableScript.hash }

@[instance_reducible]

instance Unicode.Script.instInhabited : Inhabited Script

Default value is Zzzz (Unknown)

Equations

• Unicode.Script.instInhabited = { default := { code := (('Z'.val <<< 8 ||| 'z'.val) <<< 8 ||| 'z'.val) <<< 8 ||| 'z'.val, is_valid := Unicode.Script.instInhabited._proof_1 } }

@[extern unicode_script_to_abbrev]

def Unicode.Script.toAbbrev : Script → String

String abbreviation of script

Equations

• { code := a, is_valid := a_1 }.toAbbrev = String.ofList [Char.ofUInt8 (a >>> 24).toUInt8, Char.ofUInt8 (a >>> 16).toUInt8, Char.ofUInt8 (a >>> 8).toUInt8, Char.ofUInt8 a.toUInt8]

def Unicode.Script.ofAbbrev? (abbr : String.Slice) : Option Script

Get script from abbreviation

Equations

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

@[inline]

def Unicode.Script.ofAbbrev! (abbr : String.Slice) : Script

Get script from abbreviation

Equations

• Unicode.Script.ofAbbrev! abbr = (Unicode.Script.ofAbbrev? abbr).get!

def Unicode.ScriptSet.isSorted (a : Array Script) : Bool

Check if an array of scripts is strictly sorted by script code

Equations

• Unicode.ScriptSet.isSorted a = Unicode.ScriptSet.isSorted.loop a.toList

def Unicode.ScriptSet.isSorted.loop : List Script → Bool

Equations

• Unicode.ScriptSet.isSorted.loop (s₁ :: s₂ :: ss) = (decide (s₁.code < s₂.code) && Unicode.ScriptSet.isSorted.loop (s₂ :: ss))
• Unicode.ScriptSet.isSorted.loop a✝ = true

structure Unicode.ScriptSet : Type

Set of scripts, such as the scripts a character is commonly used with

• toArray : Array Script

  Scripts in the set, sorted by script code

• is_sorted : isSorted self.toArray = true

def Unicode.instBEqScriptSet.beq : ScriptSet → ScriptSet → Bool

Equations

• One or more equations did not get rendered due to their size.
• Unicode.instBEqScriptSet.beq x✝¹ x✝ = false

@[instance_reducible]

instance Unicode.instBEqScriptSet : BEq ScriptSet

Equations

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

@[instance_reducible]

instance Unicode.ScriptSet.instInhabited : Inhabited ScriptSet

Default value is the empty set

Equations

• Unicode.ScriptSet.instInhabited = { default := { toArray := #[], is_sorted := Unicode.ScriptSet.instInhabited._proof_1 } }

@[inline]

def Unicode.ScriptSet.toList (s : ScriptSet) : List Script

List of the scripts in the set, sorted by script code

Equations

• s.toList = s.toArray.toList

def Unicode.ScriptSet.toAbbrev (s : ScriptSet) : String

String of the script abbreviations in the set, separated by spaces

Equations

• s.toAbbrev = " ".intercalate (List.map Unicode.Script.toAbbrev s.toList)

@[inline]

def Unicode.ScriptSet.contains (s : ScriptSet) (sc : Script) : Bool

Check whether a script is in the set

Equations

• s.contains sc = s.toArray.contains sc

@[instance_reducible]

instance Unicode.ScriptSet.instMembershipScript : Membership Script ScriptSet

Equations

• Unicode.ScriptSet.instMembershipScript = { mem := fun (s : Unicode.ScriptSet) (sc : Unicode.Script) => s.contains sc = true }

@[instance_reducible]

instance Unicode.ScriptSet.instDecidableMemScript (sc : Script) (s : ScriptSet) : Decidable (sc ∈ s)

Equations

• Unicode.ScriptSet.instDecidableMemScript sc s = instDecidableEqBool (s.contains sc) true