def Parser.Char.Unicode.alpha {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse alphabetic letter character

Equations

• Parser.Char.Unicode.alpha = Parser.withErrorMessage "expected letter" (Parser.tokenFilter Unicode.isAlpha)

def Parser.Char.Unicode.lowercase {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse lowercase letter character

Equations

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

def Parser.Char.Unicode.math {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse math symbol character

Equations

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

def Parser.Char.Unicode.uppercase {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse uppercase letter character

Equations

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

def Parser.Char.Unicode.whitespace {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse whitespace character

Equations

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

def Parser.Char.Unicode.digit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 10)

parse decimal digit character

Equations

• Parser.Char.Unicode.digit = Parser.withErrorMessage "expected decimal digit" (Parser.tokenMap Unicode.getDigit?)

def Parser.Char.Unicode.hexDigit {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m (Fin 16)

parse hexadecimal digit character

Equations

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

General Category

def Parser.Char.Unicode.parseGeneralCategory {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] (category : Unicode.GeneralCategory) : ParserT ε σ Char m Char

parse character from given general category

Equations

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

def Parser.Char.Unicode.GeneralCategory.letter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse letter (general category L)

Equations

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

def Parser.Char.Unicode.GeneralCategory.casedLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse cased letter (general category LC)

Equations

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

def Parser.Char.Unicode.GeneralCategory.lowercaseLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse lowercase letter (general category Ll)

Equations

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

def Parser.Char.Unicode.GeneralCategory.uppercaseLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse uppercase letter (general category Lu)

Equations

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

def Parser.Char.Unicode.GeneralCategory.titlecaseLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse titlecase letter (general category Lt)

Equations

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

def Parser.Char.Unicode.GeneralCategory.modifierLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other letter (general category Lm)

Equations

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

def Parser.Char.Unicode.GeneralCategory.otherLetter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other letter (general category Lo)

Equations

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

def Parser.Char.Unicode.GeneralCategory.mark {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse mark (general category M)

Equations

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

def Parser.Char.Unicode.GeneralCategory.spacingMark {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse spacing combining mark (general category Mc)

Equations

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

def Parser.Char.Unicode.GeneralCategory.nonspacingMark {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse nonspacing combining mark (general category Mn)

Equations

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

def Parser.Char.Unicode.GeneralCategory.enclosingMark {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse enclosing combining mark (general category Me)

Equations

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

def Parser.Char.Unicode.GeneralCategory.number {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse number (general category N)

Equations

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

def Parser.Char.Unicode.GeneralCategory.decimalNumber {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse decimal number (general category Nd)

Equations

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

def Parser.Char.Unicode.GeneralCategory.letterNumber {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse letter number (general category Nl)

Equations

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

def Parser.Char.Unicode.GeneralCategory.otherNumber {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other number (general category No)

Equations

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

def Parser.Char.Unicode.GeneralCategory.punctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse punctuation (general category P)

Equations

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

def Parser.Char.Unicode.GeneralCategory.connectorPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse connector punctuation (general category Pc)

Equations

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

def Parser.Char.Unicode.GeneralCategory.dashPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse dash punctuation (general category Pd)

Equations

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

def Parser.Char.Unicode.GeneralCategory.openPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse opening punctuation (general category Ps)

Equations

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

def Parser.Char.Unicode.GeneralCategory.closePunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse closing punctuation (general category Pe)

Equations

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

def Parser.Char.Unicode.GeneralCategory.initialPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse initial punctuation (general category Pi)

Equations

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

def Parser.Char.Unicode.GeneralCategory.finalPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse final punctuation (general category Pf)

Equations

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

def Parser.Char.Unicode.GeneralCategory.otherPunctuation {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other punctuation (general category Po)

Equations

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

def Parser.Char.Unicode.GeneralCategory.symbol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse symbol (general category S)

Equations

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

def Parser.Char.Unicode.GeneralCategory.mathSymbol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse math symbol (general category Sm)

Equations

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

def Parser.Char.Unicode.GeneralCategory.currencySymbol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse currency symbol (general category Sc)

Equations

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

def Parser.Char.Unicode.GeneralCategory.modifierSymbol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse modifier symbol (general category Sk)

Equations

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

def Parser.Char.Unicode.GeneralCategory.otherSymbol {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other symbol (general category So)

Equations

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

def Parser.Char.Unicode.GeneralCategory.separator {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse separator (general category Z)

Equations

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

def Parser.Char.Unicode.GeneralCategory.spaceSeparator {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse space separator (general category Zs)

Equations

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

def Parser.Char.Unicode.GeneralCategory.lineSeparator {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse line separator (general category Zl)

Equations

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

def Parser.Char.Unicode.GeneralCategory.paragraphSeparator {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse paragraph separator (general category Zp)

Equations

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

def Parser.Char.Unicode.GeneralCategory.other {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse other character (general category C)

Equations

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

def Parser.Char.Unicode.GeneralCategory.control {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse control character (general category Cc)

Equations

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

def Parser.Char.Unicode.GeneralCategory.format {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse format character (general category Cf)

Equations

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

def Parser.Char.Unicode.GeneralCategory.surrogate {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse surrogate character (general category Cs)

Equations

• Parser.Char.Unicode.GeneralCategory.surrogate = Parser.withErrorMessage "expected surrogate character (Cs)" (Parser.tokenFilter Unicode.GeneralCategory.isSurrogate)

def Parser.Char.Unicode.GeneralCategory.privateUse {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse private-use character (general category Co)

Equations

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

def Parser.Char.Unicode.GeneralCategory.noncharacter {ε σ : Type} {m : Type → Type u_1} [Parser.Stream σ Char] [Parser.Error ε σ Char] [Monad m] : ParserT ε σ Char m Char

parse unassigned character (general category Cn)

Equations

• Parser.Char.Unicode.GeneralCategory.noncharacter = Parser.withErrorMessage "expected unassigned character (Cn)" (Parser.tokenFilter Unicode.GeneralCategory.isUnassigned)