Unicode character parsers

Parsers for Unicode character properties, using the UnicodeBasic tables: general categories, scripts and script extensions, binary properties, and case-insensitive matching.

def ParseIt.Char.Unicode.alpha {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse alphabetic character (Unicode property Alphabetic).

Equations

• ParseIt.Char.Unicode.alpha = ParseIt.withErrorMessage "expected alphabetic character" (ParseIt.tokenFilter Unicode.isAlpha)

def ParseIt.Char.Unicode.lowercase {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse lowercase character (Unicode property Lowercase).

Equations

• ParseIt.Char.Unicode.lowercase = ParseIt.withErrorMessage "expected lowercase letter" (ParseIt.tokenFilter Unicode.isLowercase)

def ParseIt.Char.Unicode.math {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse math character (Unicode property Math).

Equations

• ParseIt.Char.Unicode.math = ParseIt.withErrorMessage "expected math symbol" (ParseIt.tokenFilter Unicode.isMath)

def ParseIt.Char.Unicode.uppercase {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse uppercase character (Unicode property Uppercase).

Equations

• ParseIt.Char.Unicode.uppercase = ParseIt.withErrorMessage "expected uppercase letter" (ParseIt.tokenFilter Unicode.isUppercase)

def ParseIt.Char.Unicode.whitespace {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse white space character (Unicode property White_Space).

Equations

• ParseIt.Char.Unicode.whitespace = ParseIt.withErrorMessage "expected whitespace" (ParseIt.tokenFilter Unicode.isWhiteSpace)

def ParseIt.Char.Unicode.digit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 10)

Parse decimal digit character (general category Nd). Other digits, such as superscripts, are rejected.

Equations

• ParseIt.Char.Unicode.digit = ParseIt.withErrorMessage "expected decimal digit" (ParseIt.tokenMap fun (c : Char) => if Unicode.isDecimal c = true then Unicode.getDigit? c else none)

def ParseIt.Char.Unicode.hexDigit {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m (Fin 16)

Parse hexadecimal digit character.

Equations

• ParseIt.Char.Unicode.hexDigit = ParseIt.withErrorMessage "expected hexadecimal digit" (ParseIt.tokenMap Unicode.getHexDigit?)

def ParseIt.Char.Unicode.noncharacter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse noncharacter code point (Unicode property Noncharacter_Code_Point).

Equations

• ParseIt.Char.Unicode.noncharacter = ParseIt.withErrorMessage "expected noncharacter code point" (ParseIt.tokenFilter Unicode.isNoncharacterCodePoint)

def ParseIt.Char.Unicode.defaultIgnorable {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse default ignorable code point (Unicode property Default_Ignorable_Code_Point).

Equations

• ParseIt.Char.Unicode.defaultIgnorable = ParseIt.withErrorMessage "expected default ignorable code point" (ParseIt.tokenFilter Unicode.isDefaultIgnorableCodePoint)

def ParseIt.Char.Unicode.ascii {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse ASCII character, U+0000 to U+007F.

Equations

• ParseIt.Char.Unicode.ascii = ParseIt.withErrorMessage "expected ASCII character" (ParseIt.tokenFilter fun (c : Char) => decide (c.val < 128))

def ParseIt.Char.Unicode.assigned {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse assigned character, any general category except Cn.

Equations

• ParseIt.Char.Unicode.assigned = ParseIt.withErrorMessage "expected assigned character" (ParseIt.tokenFilter fun (c : Char) => !Unicode.GeneralCategory.isUnassigned c)

def ParseIt.Char.Unicode.joinControl {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse join control character, U+200C or U+200D (Unicode property Join_Control).

Equations

• ParseIt.Char.Unicode.joinControl = ParseIt.withErrorMessage "expected join control character" (ParseIt.tokenFilter fun (c : Char) => c == '‌' || c == '‍')

Case-insensitive matching

def ParseIt.Char.Unicode.charCaseInsensitive {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (c : Char) : ParserT ε ι Char m Char

charCaseInsensitive c accepts and returns a character that matches c under simple case folding (Unicode property Simple_Case_Folding).

Equations

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

def ParseIt.Char.Unicode.stringCaseInsensitive {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (s : String) : ParserT ε ι Char m String

stringCaseInsensitive s accepts input whose full case folding (Unicode property Case_Folding, statuses C and F) equals s, and returns the input that matched. The pattern s is expected to be case folded already, for example "strasse" matches "Straße" and "STRASSE".

Equations

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

Scripts

def ParseIt.Char.Unicode.parseScript {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (sc : Unicode.Script) : ParserT ε ι Char m Char

Parse character of script sc (Unicode property Script).

Equations

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

def ParseIt.Char.Unicode.parseScriptExt {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (sc : Unicode.Script) : ParserT ε ι Char m Char

Parse character commonly used with script sc (Unicode property Script_Extensions).

This differs from parseScript sc: for example, U+0951 DEVANAGARI STRESS SIGN UDATTA has script Zinh (Inherited) but is accepted by parseScriptExt for Deva, Beng and others.

Equations

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

General Category

def ParseIt.Char.Unicode.parseGeneralCategory {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] (category : Unicode.GC) : ParserT ε ι Char m Char

Parse character from given general category.

Equations

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

def ParseIt.Char.Unicode.GeneralCategory.letter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse letter (general category L).

Equations

• ParseIt.Char.Unicode.GeneralCategory.letter = ParseIt.withErrorMessage "expected letter (L)" (ParseIt.tokenFilter Unicode.GeneralCategory.isLetter)

def ParseIt.Char.Unicode.GeneralCategory.casedLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse cased letter (general category LC).

Equations

• ParseIt.Char.Unicode.GeneralCategory.casedLetter = ParseIt.withErrorMessage "expected cased letter (LC)" (ParseIt.tokenFilter Unicode.GeneralCategory.isCasedLetter)

def ParseIt.Char.Unicode.GeneralCategory.lowercaseLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse lowercase letter (general category Ll).

Equations

• ParseIt.Char.Unicode.GeneralCategory.lowercaseLetter = ParseIt.withErrorMessage "expected lowercase letter (Ll)" (ParseIt.tokenFilter Unicode.GeneralCategory.isLowercaseLetter)

def ParseIt.Char.Unicode.GeneralCategory.uppercaseLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse uppercase letter (general category Lu).

Equations

• ParseIt.Char.Unicode.GeneralCategory.uppercaseLetter = ParseIt.withErrorMessage "expected uppercase letter (Lu)" (ParseIt.tokenFilter Unicode.GeneralCategory.isUppercaseLetter)

def ParseIt.Char.Unicode.GeneralCategory.titlecaseLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse titlecase letter (general category Lt).

Equations

• ParseIt.Char.Unicode.GeneralCategory.titlecaseLetter = ParseIt.withErrorMessage "expected titlecase letter (Lt)" (ParseIt.tokenFilter Unicode.GeneralCategory.isTitlecaseLetter)

def ParseIt.Char.Unicode.GeneralCategory.modifierLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other letter (general category Lm).

Equations

• ParseIt.Char.Unicode.GeneralCategory.modifierLetter = ParseIt.withErrorMessage "expected modifier letter (Lm)" (ParseIt.tokenFilter Unicode.GeneralCategory.isModifierLetter)

def ParseIt.Char.Unicode.GeneralCategory.otherLetter {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other letter (general category Lo).

Equations

• ParseIt.Char.Unicode.GeneralCategory.otherLetter = ParseIt.withErrorMessage "expected other letter (Lo)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOtherLetter)

def ParseIt.Char.Unicode.GeneralCategory.mark {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse mark (general category M).

Equations

• ParseIt.Char.Unicode.GeneralCategory.mark = ParseIt.withErrorMessage "expected mark (M)" (ParseIt.tokenFilter Unicode.GeneralCategory.isMark)

def ParseIt.Char.Unicode.GeneralCategory.spacingMark {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse spacing combining mark (general category Mc).

Equations

• ParseIt.Char.Unicode.GeneralCategory.spacingMark = ParseIt.withErrorMessage "expected spacing mark (Mc)" (ParseIt.tokenFilter Unicode.GeneralCategory.isSpacingMark)

def ParseIt.Char.Unicode.GeneralCategory.nonspacingMark {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse nonspacing combining mark (general category Mn).

Equations

• ParseIt.Char.Unicode.GeneralCategory.nonspacingMark = ParseIt.withErrorMessage "expected nonspacing mark (Mn)" (ParseIt.tokenFilter Unicode.GeneralCategory.isNonspacingMark)

def ParseIt.Char.Unicode.GeneralCategory.enclosingMark {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse enclosing combining mark (general category Me).

Equations

• ParseIt.Char.Unicode.GeneralCategory.enclosingMark = ParseIt.withErrorMessage "expected enclosing mark (Me)" (ParseIt.tokenFilter Unicode.GeneralCategory.isEnclosingMark)

def ParseIt.Char.Unicode.GeneralCategory.number {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse number (general category N).

Equations

• ParseIt.Char.Unicode.GeneralCategory.number = ParseIt.withErrorMessage "expected number (N)" (ParseIt.tokenFilter Unicode.GeneralCategory.isNumber)

def ParseIt.Char.Unicode.GeneralCategory.decimalNumber {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse decimal number (general category Nd).

Equations

• ParseIt.Char.Unicode.GeneralCategory.decimalNumber = ParseIt.withErrorMessage "expected decimal number (Nd)" (ParseIt.tokenFilter Unicode.GeneralCategory.isDecimalNumber)

def ParseIt.Char.Unicode.GeneralCategory.letterNumber {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse letter number (general category Nl).

Equations

• ParseIt.Char.Unicode.GeneralCategory.letterNumber = ParseIt.withErrorMessage "expected letter number (Nl)" (ParseIt.tokenFilter Unicode.GeneralCategory.isLetterNumber)

def ParseIt.Char.Unicode.GeneralCategory.otherNumber {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other number (general category No).

Equations

• ParseIt.Char.Unicode.GeneralCategory.otherNumber = ParseIt.withErrorMessage "expected other number (No)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOtherNumber)

def ParseIt.Char.Unicode.GeneralCategory.punctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse punctuation (general category P).

Equations

• ParseIt.Char.Unicode.GeneralCategory.punctuation = ParseIt.withErrorMessage "expected punctuation (P)" (ParseIt.tokenFilter Unicode.GeneralCategory.isPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.connectorPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse connector punctuation (general category Pc).

Equations

• ParseIt.Char.Unicode.GeneralCategory.connectorPunctuation = ParseIt.withErrorMessage "expected connector punctuation (Pc)" (ParseIt.tokenFilter Unicode.GeneralCategory.isConnectorPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.dashPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse dash punctuation (general category Pd).

Equations

• ParseIt.Char.Unicode.GeneralCategory.dashPunctuation = ParseIt.withErrorMessage "expected dash punctuation (Pd)" (ParseIt.tokenFilter Unicode.GeneralCategory.isDashPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.openPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse opening punctuation (general category Ps).

Equations

• ParseIt.Char.Unicode.GeneralCategory.openPunctuation = ParseIt.withErrorMessage "expected opening punctuation (Ps)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOpenPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.closePunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse closing punctuation (general category Pe).

Equations

• ParseIt.Char.Unicode.GeneralCategory.closePunctuation = ParseIt.withErrorMessage "expected opening punctuation (Pe)" (ParseIt.tokenFilter Unicode.GeneralCategory.isClosePunctuation)

def ParseIt.Char.Unicode.GeneralCategory.initialPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse initial punctuation (general category Pi).

Equations

• ParseIt.Char.Unicode.GeneralCategory.initialPunctuation = ParseIt.withErrorMessage "expected initial punctuation (Pi)" (ParseIt.tokenFilter Unicode.GeneralCategory.isInitialPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.finalPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse final punctuation (general category Pf).

Equations

• ParseIt.Char.Unicode.GeneralCategory.finalPunctuation = ParseIt.withErrorMessage "expected final punctuation (Pf)" (ParseIt.tokenFilter Unicode.GeneralCategory.isFinalPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.otherPunctuation {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other punctuation (general category Po).

Equations

• ParseIt.Char.Unicode.GeneralCategory.otherPunctuation = ParseIt.withErrorMessage "expected other punctuation (Po)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOtherPunctuation)

def ParseIt.Char.Unicode.GeneralCategory.symbol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse symbol (general category S).

Equations

• ParseIt.Char.Unicode.GeneralCategory.symbol = ParseIt.withErrorMessage "expected symbol (S)" (ParseIt.tokenFilter Unicode.GeneralCategory.isSymbol)

def ParseIt.Char.Unicode.GeneralCategory.mathSymbol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse math symbol (general category Sm).

Equations

• ParseIt.Char.Unicode.GeneralCategory.mathSymbol = ParseIt.withErrorMessage "expected math symbol (Sm)" (ParseIt.tokenFilter Unicode.GeneralCategory.isMathSymbol)

def ParseIt.Char.Unicode.GeneralCategory.currencySymbol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse currency symbol (general category Sc).

Equations

• ParseIt.Char.Unicode.GeneralCategory.currencySymbol = ParseIt.withErrorMessage "expected currency symbol (Sc)" (ParseIt.tokenFilter Unicode.GeneralCategory.isCurrencySymbol)

def ParseIt.Char.Unicode.GeneralCategory.modifierSymbol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse modifier symbol (general category Sk).

Equations

• ParseIt.Char.Unicode.GeneralCategory.modifierSymbol = ParseIt.withErrorMessage "expected modifier symbol (Sk)" (ParseIt.tokenFilter Unicode.GeneralCategory.isModifierSymbol)

def ParseIt.Char.Unicode.GeneralCategory.otherSymbol {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other symbol (general category So).

Equations

• ParseIt.Char.Unicode.GeneralCategory.otherSymbol = ParseIt.withErrorMessage "expected other symbol (So)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOtherSymbol)

def ParseIt.Char.Unicode.GeneralCategory.separator {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse separator (general category Z).

Equations

• ParseIt.Char.Unicode.GeneralCategory.separator = ParseIt.withErrorMessage "expected separator (Z)" (ParseIt.tokenFilter Unicode.GeneralCategory.isSeparator)

def ParseIt.Char.Unicode.GeneralCategory.spaceSeparator {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse space separator (general category Zs).

Equations

• ParseIt.Char.Unicode.GeneralCategory.spaceSeparator = ParseIt.withErrorMessage "expected space separator (Zs)" (ParseIt.tokenFilter Unicode.GeneralCategory.isSpaceSeparator)

def ParseIt.Char.Unicode.GeneralCategory.lineSeparator {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse line separator (general category Zl).

Equations

• ParseIt.Char.Unicode.GeneralCategory.lineSeparator = ParseIt.withErrorMessage "expected line separator (Zl)" (ParseIt.tokenFilter Unicode.GeneralCategory.isLineSeparator)

def ParseIt.Char.Unicode.GeneralCategory.paragraphSeparator {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse paragraph separator (general category Zp).

Equations

• ParseIt.Char.Unicode.GeneralCategory.paragraphSeparator = ParseIt.withErrorMessage "expected paragraph separator (Zp)" (ParseIt.tokenFilter Unicode.GeneralCategory.isParagraphSeparator)

def ParseIt.Char.Unicode.GeneralCategory.other {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse other character (general category C).

Equations

• ParseIt.Char.Unicode.GeneralCategory.other = ParseIt.withErrorMessage "expected other character (C)" (ParseIt.tokenFilter Unicode.GeneralCategory.isOther)

def ParseIt.Char.Unicode.GeneralCategory.control {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse control character (general category Cc).

Equations

• ParseIt.Char.Unicode.GeneralCategory.control = ParseIt.withErrorMessage "expected control character (Cc)" (ParseIt.tokenFilter Unicode.GeneralCategory.isControl)

def ParseIt.Char.Unicode.GeneralCategory.format {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse format character (general category Cf).

Equations

• ParseIt.Char.Unicode.GeneralCategory.format = ParseIt.withErrorMessage "expected format character (Cf)" (ParseIt.tokenFilter Unicode.GeneralCategory.isFormat)

def ParseIt.Char.Unicode.GeneralCategory.privateUse {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse private-use character (general category Co).

Equations

• ParseIt.Char.Unicode.GeneralCategory.privateUse = ParseIt.withErrorMessage "expected private-use character (Co)" (ParseIt.tokenFilter Unicode.GeneralCategory.isPrivateUse)

def ParseIt.Char.Unicode.GeneralCategory.unassigned {ε ι : Type} {m : Type → Type} [Std.Iterator ι Id Char] [Std.Iterators.Productive ι Id] [Error ε ι Char] [Monad m] : ParserT ε ι Char m Char

Parse unassigned code point (general category Cn).

Equations

• ParseIt.Char.Unicode.GeneralCategory.unassigned = ParseIt.withErrorMessage "expected unassigned code point (Cn)" (ParseIt.tokenFilter Unicode.GeneralCategory.isUnassigned)