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.instInhabitedMajorGeneralCategory.default }

def Unicode.instInhabitedMajorGeneralCategory.default : MajorGeneralCategory

Equations

• Unicode.instInhabitedMajorGeneralCategory.default = Unicode.MajorGeneralCategory.letter

instance Unicode.instDecidableEqMajorGeneralCategory : DecidableEq MajorGeneralCategory

Equations

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

def Unicode.instDecidableEqMinorGeneralCategory.decEq {a✝ : MajorGeneralCategory} (x✝ x✝¹ : MinorGeneralCategory a✝) : Decidable (x✝ = x✝¹)

Equations

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

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

Equations

• Unicode.instDecidableEqMinorGeneralCategory = Unicode.instDecidableEqMinorGeneralCategory.decEq

def Unicode.GC : Type

General category (GC)

Unicode property: General_Category

Equations

• Unicode.GC = UInt32

instance Unicode.instDecidableEqGC : DecidableEq GC

Equations

• Unicode.instDecidableEqGC = instDecidableEqUInt32

instance Unicode.instInhabitedGC : Inhabited GC

Equations

• Unicode.instInhabitedGC = instInhabitedUInt32

instance Unicode.GC.instOrOp : OrOp GC

Equations

• Unicode.GC.instOrOp = inferInstanceAs (OrOp UInt32)

instance Unicode.GC.instAndOp : AndOp GC

Equations

• Unicode.GC.instAndOp = inferInstanceAs (AndOp UInt32)

instance Unicode.GC.instComplement : Complement GC

Equations

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

instance Unicode.GC.instHasSubset : HasSubset GC

Equations

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

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

Equations

• x.instDecidableSubset y = inferInstanceAs (Decidable ((x &&& y == x) = true))

def Unicode.GC.none : GC

Equations

• Unicode.GC.none = 0

def Unicode.GC.univ : GC

Equations

• Unicode.GC.univ = 1073741823

def Unicode.GC.Lu : GC

Equations

• Unicode.GC.Lu = 1

def Unicode.GC.Ll : GC

Equations

• Unicode.GC.Ll = 2

def Unicode.GC.Lt : GC

Equations

• Unicode.GC.Lt = 4

def Unicode.GC.Lm : GC

Equations

• Unicode.GC.Lm = 8

def Unicode.GC.Lo : GC

Equations

• Unicode.GC.Lo = 16

def Unicode.GC.LC : GC

Equations

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

def Unicode.GC.L : GC

Equations

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

def Unicode.GC.Mn : GC

Equations

• Unicode.GC.Mn = 32

def Unicode.GC.Mc : GC

Equations

• Unicode.GC.Mc = 64

def Unicode.GC.Me : GC

Equations

• Unicode.GC.Me = 128

def Unicode.GC.M : GC

Equations

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

def Unicode.GC.Nd : GC

Equations

• Unicode.GC.Nd = 256

def Unicode.GC.Nl : GC

Equations

• Unicode.GC.Nl = 512

def Unicode.GC.No : GC

Equations

• Unicode.GC.No = 1024

def Unicode.GC.N : GC

Equations

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

def Unicode.GC.Pc : GC

Equations

• Unicode.GC.Pc = 2048

def Unicode.GC.Pd : GC

Equations

• Unicode.GC.Pd = 4096

def Unicode.GC.Ps : GC

Equations

• Unicode.GC.Ps = 8192

def Unicode.GC.Pe : GC

Equations

• Unicode.GC.Pe = 16384

def Unicode.GC.Pi : GC

Equations

• Unicode.GC.Pi = 32768

def Unicode.GC.Pf : GC

Equations

• Unicode.GC.Pf = 65536

def Unicode.GC.Po : GC

Equations

• Unicode.GC.Po = 131072

def Unicode.GC.PG : GC

Equations

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

def Unicode.GC.PQ : GC

Equations

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

def 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

def Unicode.GC.Sm : GC

Equations

• Unicode.GC.Sm = 262144

def Unicode.GC.Sc : GC

Equations

• Unicode.GC.Sc = 524288

def Unicode.GC.Sk : GC

Equations

• Unicode.GC.Sk = 1048576

def Unicode.GC.So : GC

Equations

• Unicode.GC.So = 2097152

def Unicode.GC.S : GC

Equations

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

def Unicode.GC.Zs : GC

Equations

• Unicode.GC.Zs = 4194304

def Unicode.GC.Zl : GC

Equations

• Unicode.GC.Zl = 8388608

def Unicode.GC.Zp : GC

Equations

• Unicode.GC.Zp = 16777216

def Unicode.GC.Z : GC

Equations

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

def Unicode.GC.Cc : GC

Equations

• Unicode.GC.Cc = 33554432

def Unicode.GC.Cf : GC

Equations

• Unicode.GC.Cf = 67108864

def Unicode.GC.Cs : GC

Equations

• Unicode.GC.Cs = 134217728

def Unicode.GC.Co : GC

Equations

• Unicode.GC.Co = 268435456

def Unicode.GC.Cn : GC

Equations

• Unicode.GC.Cn = 536870912

def Unicode.GC.C : GC

Equations

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

def Unicode.GC.mk (major : MajorGeneralCategory) : Option (MinorGeneralCategory major) → GC

Equations

• Unicode.GC.mk Unicode.MajorGeneralCategory.letter none = Unicode.GC.L
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.casedLetter) = Unicode.GC.LC
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.uppercaseLetter) = Unicode.GC.Lu
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.lowercaseLetter) = Unicode.GC.Ll
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.titlecaseLetter) = Unicode.GC.Lt
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.modifierLetter) = Unicode.GC.Lm
• Unicode.GC.mk Unicode.MajorGeneralCategory.letter (some Unicode.MinorGeneralCategory.otherLetter) = Unicode.GC.Lo
• Unicode.GC.mk Unicode.MajorGeneralCategory.mark none = Unicode.GC.M
• Unicode.GC.mk Unicode.MajorGeneralCategory.mark (some Unicode.MinorGeneralCategory.nonspacingMark) = Unicode.GC.Mn
• Unicode.GC.mk Unicode.MajorGeneralCategory.mark (some Unicode.MinorGeneralCategory.spacingMark) = Unicode.GC.Mc
• Unicode.GC.mk Unicode.MajorGeneralCategory.mark (some Unicode.MinorGeneralCategory.enclosingMark) = Unicode.GC.Me
• Unicode.GC.mk Unicode.MajorGeneralCategory.number none = Unicode.GC.N
• Unicode.GC.mk Unicode.MajorGeneralCategory.number (some Unicode.MinorGeneralCategory.decimalNumber) = Unicode.GC.Nd
• Unicode.GC.mk Unicode.MajorGeneralCategory.number (some Unicode.MinorGeneralCategory.letterNumber) = Unicode.GC.Nl
• Unicode.GC.mk Unicode.MajorGeneralCategory.number (some Unicode.MinorGeneralCategory.otherNumber) = Unicode.GC.No
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation none = Unicode.GC.P
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.connectorPunctuation) = Unicode.GC.Pc
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.dashPunctuation) = Unicode.GC.Pd
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.groupPunctuation) = Unicode.GC.PG
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.openPunctuation) = Unicode.GC.Ps
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.closePunctuation) = Unicode.GC.Pe
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.quotePunctuation) = Unicode.GC.PQ
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.initialPunctuation) = Unicode.GC.Pi
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.finalPunctuation) = Unicode.GC.Pf
• Unicode.GC.mk Unicode.MajorGeneralCategory.punctuation (some Unicode.MinorGeneralCategory.otherPunctuation) = Unicode.GC.Po
• Unicode.GC.mk Unicode.MajorGeneralCategory.symbol none = Unicode.GC.S
• Unicode.GC.mk Unicode.MajorGeneralCategory.symbol (some Unicode.MinorGeneralCategory.mathSymbol) = Unicode.GC.Sm
• Unicode.GC.mk Unicode.MajorGeneralCategory.symbol (some Unicode.MinorGeneralCategory.currencySymbol) = Unicode.GC.Sc
• Unicode.GC.mk Unicode.MajorGeneralCategory.symbol (some Unicode.MinorGeneralCategory.modifierSymbol) = Unicode.GC.Sk
• Unicode.GC.mk Unicode.MajorGeneralCategory.symbol (some Unicode.MinorGeneralCategory.otherSymbol) = Unicode.GC.So
• Unicode.GC.mk Unicode.MajorGeneralCategory.separator none = Unicode.GC.Z
• Unicode.GC.mk Unicode.MajorGeneralCategory.separator (some Unicode.MinorGeneralCategory.spaceSeparator) = Unicode.GC.Zs
• Unicode.GC.mk Unicode.MajorGeneralCategory.separator (some Unicode.MinorGeneralCategory.lineSeparator) = Unicode.GC.Zl
• Unicode.GC.mk Unicode.MajorGeneralCategory.separator (some Unicode.MinorGeneralCategory.paragraphSeparator) = Unicode.GC.Zp
• Unicode.GC.mk Unicode.MajorGeneralCategory.other none = Unicode.GC.C
• Unicode.GC.mk Unicode.MajorGeneralCategory.other (some Unicode.MinorGeneralCategory.control) = Unicode.GC.Cc
• Unicode.GC.mk Unicode.MajorGeneralCategory.other (some Unicode.MinorGeneralCategory.format) = Unicode.GC.Cf
• Unicode.GC.mk Unicode.MajorGeneralCategory.other (some Unicode.MinorGeneralCategory.surrogate) = Unicode.GC.Cs
• Unicode.GC.mk Unicode.MajorGeneralCategory.other (some Unicode.MinorGeneralCategory.privateUse) = Unicode.GC.Co
• Unicode.GC.mk Unicode.MajorGeneralCategory.other (some Unicode.MinorGeneralCategory.unassigned) = 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!" 403 9 "invalid general category"

instance Unicode.GC.instRepr : Repr GC

Equations

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

instance Unicode.GC.instToString : ToString GC

Equations

• Unicode.GC.instToString = { toString := fun (x : Unicode.GC) => " | ".intercalate (Unicode.GC.reprAux✝ x) }

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

Equations

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

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

Equations

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

def Unicode.GC.ofString? (s : Substring) : Option GC

Equations

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

def Unicode.GC.ofString! (s : Substring) : GC

Equations

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

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

structure Unicode.GeneralCategory : Type

• 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 := Unicode.instInhabitedGeneralCategory.default }

def Unicode.instInhabitedGeneralCategory.default : GeneralCategory

Equations

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

instance Unicode.instDecidableEqGeneralCategory : DecidableEq GeneralCategory

Equations

• Unicode.instDecidableEqGeneralCategory = Unicode.instDecidableEqGeneralCategory.decEq

def Unicode.instDecidableEqGeneralCategory.decEq (x✝ x✝¹ : GeneralCategory) : Decidable (x✝ = x✝¹)

Equations

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

@[deprecated Unicode.GC.L (since := "1.2.0")]

def Unicode.GeneralCategory.L : GeneralCategory

General category: letter (L)

Equations

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

@[deprecated Unicode.GC.LC (since := "1.2.0")]

def Unicode.GeneralCategory.LC : GeneralCategory

General category: cased letter (LC)

Equations

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

@[deprecated Unicode.GC.Lu (since := "1.2.0")]

def Unicode.GeneralCategory.Lu : GeneralCategory

General category: uppercase letter (Lu)

Equations

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

@[deprecated Unicode.GC.Ll (since := "1.2.0")]

def Unicode.GeneralCategory.Ll : GeneralCategory

General category: lowercase letter (Ll)

Equations

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

@[deprecated Unicode.GC.Lt (since := "1.2.0")]

def Unicode.GeneralCategory.Lt : GeneralCategory

General category: titlecase letter (Lt)

Equations

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

@[deprecated Unicode.GC.Lm (since := "1.2.0")]

def Unicode.GeneralCategory.Lm : GeneralCategory

General category: modifier letter (Lm)

Equations

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

@[deprecated Unicode.GC.Lo (since := "1.2.0")]

def Unicode.GeneralCategory.Lo : GeneralCategory

General category: other letter (Lo)

Equations

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

@[deprecated Unicode.GC.M (since := "1.2.0")]

def Unicode.GeneralCategory.M : GeneralCategory

General category mark (M)

Equations

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

@[deprecated Unicode.GC.Mn (since := "1.2.0")]

def Unicode.GeneralCategory.Mn : GeneralCategory

General category: nonspacing combining mark (Mn)

Equations

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

@[deprecated Unicode.GC.Mc (since := "1.2.0")]

def Unicode.GeneralCategory.Mc : GeneralCategory

General category: spacing combining mark (Mc)

Equations

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

@[deprecated Unicode.GC.Me (since := "1.2.0")]

def Unicode.GeneralCategory.Me : GeneralCategory

General category: enclosing combining mark (Me)

Equations

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

@[deprecated Unicode.GC.N (since := "1.2.0")]

def Unicode.GeneralCategory.N : GeneralCategory

General category: number (N)

Equations

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

@[deprecated Unicode.GC.Nd (since := "1.2.0")]

def Unicode.GeneralCategory.Nd : GeneralCategory

General category: decimal digit (Nd)

Equations

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

@[deprecated Unicode.GC.Nl (since := "1.2.0")]

def Unicode.GeneralCategory.Nl : GeneralCategory

General category: letter number (Nl)

Equations

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

@[deprecated Unicode.GC.No (since := "1.2.0")]

def Unicode.GeneralCategory.No : GeneralCategory

General category: other number (No)

Equations

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

@[deprecated Unicode.GC.P (since := "1.2.0")]

def Unicode.GeneralCategory.P : GeneralCategory

General category: punctuation (P)

Equations

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

@[deprecated Unicode.GC.Pc (since := "1.2.0")]

def Unicode.GeneralCategory.Pc : GeneralCategory

General category: connector punctuation (Pc)

Equations

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

@[deprecated Unicode.GC.Pd (since := "1.2.0")]

def Unicode.GeneralCategory.Pd : GeneralCategory

General category: dash punctuation (Pd)

Equations

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

@[deprecated Unicode.GC.PG (since := "1.2.0")]

def Unicode.GeneralCategory.PG : GeneralCategory

General category: grouping punctuation (PG)

Equations

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

@[deprecated Unicode.GC.Ps (since := "1.2.0")]

def Unicode.GeneralCategory.Ps : GeneralCategory

General category: opening punctuation (Ps)

Equations

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

@[deprecated Unicode.GC.Pe (since := "1.2.0")]

def Unicode.GeneralCategory.Pe : GeneralCategory

General category: closing punctuation (Pe)

Equations

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

@[deprecated Unicode.GC.PQ (since := "1.2.0")]

def Unicode.GeneralCategory.PQ : GeneralCategory

General category: quoting punctuation (PQ)

Equations

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

@[deprecated Unicode.GC.Pi (since := "1.2.0")]

def Unicode.GeneralCategory.Pi : GeneralCategory

General category: initial punctuation (Pi)

Equations

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

@[deprecated Unicode.GC.Pf (since := "1.2.0")]

def Unicode.GeneralCategory.Pf : GeneralCategory

General category: final punctuation (Pf)

Equations

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

@[deprecated Unicode.GC.Po (since := "1.2.0")]

def Unicode.GeneralCategory.Po : GeneralCategory

General category: other punctuation (Po)

Equations

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

@[deprecated Unicode.GC.S (since := "1.2.0")]

def Unicode.GeneralCategory.S : GeneralCategory

General category: symbol (S)

Equations

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

@[deprecated Unicode.GC.Sm (since := "1.2.0")]

def Unicode.GeneralCategory.Sm : GeneralCategory

General category: math symbol (Sm)

Equations

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

@[deprecated Unicode.GC.Sc (since := "1.2.0")]

def Unicode.GeneralCategory.Sc : GeneralCategory

General category: currency symbol (Sc)

Equations

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

@[deprecated Unicode.GC.Sk (since := "1.2.0")]

def Unicode.GeneralCategory.Sk : GeneralCategory

General category: modifier symbol (Sk)

Equations

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

@[deprecated Unicode.GC.So (since := "1.2.0")]

def Unicode.GeneralCategory.So : GeneralCategory

General category: other symbol (So)

Equations

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

@[deprecated Unicode.GC.Z (since := "1.2.0")]

def Unicode.GeneralCategory.Z : GeneralCategory

General category: separator (Z)

Equations

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

@[deprecated Unicode.GC.Zs (since := "1.2.0")]

def Unicode.GeneralCategory.Zs : GeneralCategory

General category: space separator (Zs)

Equations

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

@[deprecated Unicode.GC.Zl (since := "1.2.0")]

def Unicode.GeneralCategory.Zl : GeneralCategory

General category: line separator (Zl)

Equations

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

@[deprecated Unicode.GC.Zp (since := "1.2.0")]

def Unicode.GeneralCategory.Zp : GeneralCategory

General category: paragraph separator (Zp)

Equations

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

@[deprecated Unicode.GC.C (since := "1.2.0")]

def Unicode.GeneralCategory.C : GeneralCategory

General category: other (C)

Equations

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

@[deprecated Unicode.GC.Cc (since := "1.2.0")]

def Unicode.GeneralCategory.Cc : GeneralCategory

General category: control (Cc)

Equations

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

@[deprecated Unicode.GC.Cf (since := "1.2.0")]

def Unicode.GeneralCategory.Cf : GeneralCategory

General category: format (Cf)

Equations

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

@[deprecated Unicode.GC.Cs (since := "1.2.0")]

def Unicode.GeneralCategory.Cs : GeneralCategory

General category: surrogate (Cs)

Equations

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

@[deprecated Unicode.GC.Co (since := "1.2.0")]

def Unicode.GeneralCategory.Co : GeneralCategory

General category: private use (Co)

Equations

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

@[deprecated Unicode.GC.Cn (since := "1.2.0")]

def Unicode.GeneralCategory.Cn : GeneralCategory

General category: unassigned (Cn)

Equations

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

@[deprecated Unicode.GC.toAbbrev! (since := "1.2.0")]

def Unicode.GeneralCategory.toAbbrev : GeneralCategory → String

String abbreviation for general category

Equations

• { major := Unicode.MajorGeneralCategory.letter, minor := none }.toAbbrev = "L"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.casedLetter }.toAbbrev = "LC"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.uppercaseLetter }.toAbbrev = "Lu"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.lowercaseLetter }.toAbbrev = "Ll"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.titlecaseLetter }.toAbbrev = "Lt"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.modifierLetter }.toAbbrev = "Lm"
• { major := Unicode.MajorGeneralCategory.letter, minor := some Unicode.MinorGeneralCategory.otherLetter }.toAbbrev = "Lo"
• { major := Unicode.MajorGeneralCategory.mark, minor := none }.toAbbrev = "M"
• { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.nonspacingMark }.toAbbrev = "Mn"
• { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.spacingMark }.toAbbrev = "Mc"
• { major := Unicode.MajorGeneralCategory.mark, minor := some Unicode.MinorGeneralCategory.enclosingMark }.toAbbrev = "Me"
• { major := Unicode.MajorGeneralCategory.number, minor := none }.toAbbrev = "N"
• { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.decimalNumber }.toAbbrev = "Nd"
• { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.letterNumber }.toAbbrev = "Nl"
• { major := Unicode.MajorGeneralCategory.number, minor := some Unicode.MinorGeneralCategory.otherNumber }.toAbbrev = "No"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := none }.toAbbrev = "P"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.connectorPunctuation }.toAbbrev = "Pc"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.dashPunctuation }.toAbbrev = "Pd"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.groupPunctuation }.toAbbrev = "PG"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.openPunctuation }.toAbbrev = "Ps"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.closePunctuation }.toAbbrev = "Pe"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.quotePunctuation }.toAbbrev = "PQ"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.initialPunctuation }.toAbbrev = "Pi"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.finalPunctuation }.toAbbrev = "Pf"
• { major := Unicode.MajorGeneralCategory.punctuation, minor := some Unicode.MinorGeneralCategory.otherPunctuation }.toAbbrev = "Po"
• { major := Unicode.MajorGeneralCategory.symbol, minor := none }.toAbbrev = "S"
• { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.mathSymbol }.toAbbrev = "Sm"
• { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.currencySymbol }.toAbbrev = "Sc"
• { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.modifierSymbol }.toAbbrev = "Sk"
• { major := Unicode.MajorGeneralCategory.symbol, minor := some Unicode.MinorGeneralCategory.otherSymbol }.toAbbrev = "So"
• { major := Unicode.MajorGeneralCategory.separator, minor := none }.toAbbrev = "Z"
• { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.spaceSeparator }.toAbbrev = "Zs"
• { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.lineSeparator }.toAbbrev = "Zl"
• { major := Unicode.MajorGeneralCategory.separator, minor := some Unicode.MinorGeneralCategory.paragraphSeparator }.toAbbrev = "Zp"
• { major := Unicode.MajorGeneralCategory.other, minor := none }.toAbbrev = "C"
• { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.control }.toAbbrev = "Cc"
• { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.format }.toAbbrev = "Cf"
• { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.surrogate }.toAbbrev = "Cs"
• { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.privateUse }.toAbbrev = "Co"
• { major := Unicode.MajorGeneralCategory.other, minor := some Unicode.MinorGeneralCategory.unassigned }.toAbbrev = "Cn"

@[deprecated Unicode.GC.ofAbbrev? (since := "1.2.0")]

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.

@[deprecated Unicode.GC.ofAbbrev! (since := "1.2.0")]

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

• Unicode.instReprGeneralCategory = { reprPrec := fun (gc : Unicode.GeneralCategory) (x : Nat) => Std.Format.text (toString "Unicode.GeneralCategory." ++ toString gc.toAbbrev) }

@[deprecated Option.some (since := "1.2.0")]

def Unicode.GeneralCategory.ofGC? (c : GC) : Option GeneralCategory

Equations

• Unicode.GeneralCategory.ofGC? c = match Unicode.GC.reprAux✝ c with | [a] => some (Unicode.GeneralCategory.ofAbbrev! a.toSubstring) | x => none

@[deprecated id (since := "1.2.0")]

def Unicode.GeneralCategory.ofGC! (c : GC) : GeneralCategory

Equations

• Unicode.GeneralCategory.ofGC! c = (Unicode.GeneralCategory.ofGC? c).get!

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

instance Unicode.instInhabitedNumericType : Inhabited NumericType

Equations

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

instance Unicode.instDecidableEqNumericType : DecidableEq NumericType

Equations

• Unicode.instDecidableEqNumericType = Unicode.instDecidableEqNumericType.decEq

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 ⋯

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

Equations

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

instance Unicode.instReprNumericType : Repr NumericType

Equations

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

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.instInhabitedCompatibilityTag.default }

def Unicode.instInhabitedCompatibilityTag.default : CompatibilityTag

Equations

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

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 Unicode.instReprCompatibilityTag : Repr CompatibilityTag

Equations

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

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 := Unicode.instInhabitedDecompositionMapping.default }

def Unicode.instInhabitedDecompositionMapping.default : DecompositionMapping

Equations

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

instance Unicode.instDecidableEqDecompositionMapping : DecidableEq DecompositionMapping

Equations

• Unicode.instDecidableEqDecompositionMapping = Unicode.instDecidableEqDecompositionMapping.decEq

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

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

def Unicode.instInhabitedBidiClass.default : BidiClass

Equations

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

instance Unicode.instInhabitedBidiClass : Inhabited BidiClass

Equations

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

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 : 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) }