Documentation

Unicode.General.GeneralCategory

inductive Unicode.GeneralCategory:

Type

uppercaseLetter: Unicode.GeneralCategory
lowercaseLetter: Unicode.GeneralCategory
titlecaseLetter: Unicode.GeneralCategory
casedLetter: Unicode.GeneralCategory
modifierLetter: Unicode.GeneralCategory
otherLetter: Unicode.GeneralCategory
letter: Unicode.GeneralCategory
nonspacingMark: Unicode.GeneralCategory
spacingMark: Unicode.GeneralCategory
enclosingMark: Unicode.GeneralCategory
mark: Unicode.GeneralCategory
decimalNumber: Unicode.GeneralCategory
letterNumber: Unicode.GeneralCategory
otherNumber: Unicode.GeneralCategory
number: Unicode.GeneralCategory
connectorPunctuation: Unicode.GeneralCategory
dashPunctuation: Unicode.GeneralCategory
openPunctuation: Unicode.GeneralCategory
closePunctuation: Unicode.GeneralCategory
initialPunctuation: Unicode.GeneralCategory
finalPunctuation: Unicode.GeneralCategory
otherPunctuation: Unicode.GeneralCategory
punctuation: Unicode.GeneralCategory
mathSymbol: Unicode.GeneralCategory
currencySymbol: Unicode.GeneralCategory
modifierSymbol: Unicode.GeneralCategory
otherSymbol: Unicode.GeneralCategory
symbol: Unicode.GeneralCategory
spaceSeparator: Unicode.GeneralCategory
lineSeparator: Unicode.GeneralCategory
paragraphSeparator: Unicode.GeneralCategory
separator: Unicode.GeneralCategory
control: Unicode.GeneralCategory
format: Unicode.GeneralCategory
surrogate: Unicode.GeneralCategory
privateUse: Unicode.GeneralCategory
unassigned: Unicode.GeneralCategory
other: Unicode.GeneralCategory

http://www.unicode.org/reports/tr44/#GC_Values_Table

instance Unicode.instDecidableEqGeneralCategory:

DecidableEq Unicode.GeneralCategory

Equations

Unicode.instDecidableEqGeneralCategory x y = if h : Unicode.GeneralCategory.toCtorIdx x = Unicode.GeneralCategory.toCtorIdx y then isTrue (_ : x = y) else isFalse (_ : x = y → False)

instance Unicode.instInhabitedGeneralCategory:

Inhabited Unicode.GeneralCategory

Equations

Unicode.instInhabitedGeneralCategory = { default := Unicode.GeneralCategory.uppercaseLetter }

instance Unicode.instReprGeneralCategory:

Repr Unicode.GeneralCategory

Equations

Unicode.instReprGeneralCategory = { reprPrec := [anonymous] }

def Unicode.GeneralCategory.fromString:

String → Unicode.GeneralCategory

Convert abbrevation String to GeneralCategory.

Equations

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

def Unicode.GeneralCategory.toString:

Unicode.GeneralCategory → String

Convert GeneralCategory to abbrevation String.

Equations

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

instance Unicode.GeneralCategory.instToStringGeneralCategory:

ToString Unicode.GeneralCategory

Convert GeneralCategory to abbrevation String.

Equations

Unicode.GeneralCategory.instToStringGeneralCategory = { toString := Unicode.GeneralCategory.toString }

def Unicode.getGeneralCategory (c : Char) :

Unicode.GeneralCategory

Get GeneralCategory of a Char.

NOTE: Grouping categories like letter, mark, number, punctuation, symbol, separator and other are not in return value. If you want to check if a Char is in these GeneralCategory, use charInGeneralCategory instead.

Equations

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

def Unicode.charInGeneralCategory (c : Char) (gc : Unicode.GeneralCategory) :

Check if a Char is in given GeneralCategory.

Equations

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