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

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

Unicode property: General_Category

Equations

• Unicode.GC = UInt32

@[implicit_reducible]

instance Unicode.instDecidableEqGC : DecidableEq GC

Equations

• Unicode.instDecidableEqGC = Unicode.instDecidableEqGC._aux_1

@[implicit_reducible]

instance Unicode.instInhabitedGC : Inhabited GC

Equations

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

@[implicit_reducible]

instance Unicode.GC.instOrOp : OrOp GC

Equations

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

@[implicit_reducible]

instance Unicode.GC.instAndOp : AndOp GC

Equations

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

@[implicit_reducible]

instance Unicode.GC.instComplement : Complement GC

Equations

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

@[implicit_reducible]

instance Unicode.GC.instHasSubset : HasSubset GC

Equations

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

@[implicit_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!" 278 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.

@[implicit_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)

@[implicit_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!" 334 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!" 345 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

def Unicode.instInhabitedNumericType.default : NumericType

Equations

• Unicode.instInhabitedNumericType.default = Unicode.NumericType.decimal default

@[implicit_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 ⋯

@[implicit_reducible]

instance Unicode.instDecidableEqNumericType : DecidableEq NumericType

Equations

• Unicode.instDecidableEqNumericType = Unicode.instDecidableEqNumericType.decEq

@[implicit_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

@[implicit_reducible]

instance Unicode.instInhabitedCompatibilityTag : Inhabited CompatibilityTag

Equations

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

def Unicode.instInhabitedCompatibilityTag.default : CompatibilityTag

Equations

• Unicode.instInhabitedCompatibilityTag.default = Unicode.CompatibilityTag.font

@[implicit_reducible]

instance Unicode.instDecidableEqCompatibilityTag : DecidableEq CompatibilityTag

Equations

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

@[implicit_reducible]

instance Unicode.instReprCompatibilityTag : Repr CompatibilityTag

Equations

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

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

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Unicode.instInhabitedDecompositionMapping : Inhabited DecompositionMapping

Equations

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

def Unicode.instInhabitedDecompositionMapping.default : DecompositionMapping

Equations

• Unicode.instInhabitedDecompositionMapping.default = { tag := default, mapping := 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 ⋯

@[implicit_reducible]

instance Unicode.instDecidableEqDecompositionMapping : DecidableEq DecompositionMapping

Equations

• Unicode.instDecidableEqDecompositionMapping = Unicode.instDecidableEqDecompositionMapping.decEq

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

Equations

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

@[implicit_reducible]

instance Unicode.instReprDecompositionMapping : Repr DecompositionMapping

Equations

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

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)

@[implicit_reducible]

instance Unicode.instInhabitedBidiClass : Inhabited BidiClass

Equations

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

def Unicode.instInhabitedBidiClass.default : BidiClass

Equations

• Unicode.instInhabitedBidiClass.default = Unicode.BidiClass.leftToRight

@[implicit_reducible]

instance Unicode.instDecidableEqBidiClass : DecidableEq BidiClass

Equations

• Unicode.instDecidableEqBidiClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx 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 : 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.

@[implicit_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

Equations

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

structure Unicode.Script : Type

Script identifier type

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

@[implicit_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)

@[implicit_reducible]

instance Unicode.instHashableScript : Hashable Script

Equations

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

@[implicit_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!