def Lean.Parser.optional (p : Parser) : Parser

The parser optional(p), or (p)?, parses p if it succeeds, otherwise it succeeds with no value.

Note that because ? is a legal identifier character, one must write (p)? or p ? for it to parse correctly. ident? will not work; one must write (ident)? instead.

This parser has arity 1: it produces a nullKind node containing either zero arguments (for the none case) or the list of arguments produced by p. (In particular, if p has arity 0 then the two cases are not differentiated!)

def Lean.Parser.many (p : Parser) : Parser

The parser many(p), or p*, repeats p until it fails, and returns the list of results.

The argument p is "auto-grouped", meaning that if the arity is greater than 1 it will be automatically replaced by group(p) to ensure that it produces exactly 1 value.

This parser has arity 1: it produces a nullKind node containing one argument for each invocation of p (or group(p)).

def Lean.Parser.many1 (p : Parser) : Parser

The parser many1(p), or p+, repeats p until it fails, and returns the list of results. p must succeed at least once, or this parser will fail.

Note that this parser produces the same parse tree as the many(p) / p* combinator, and one matches both p* and p+ using $[ .. ]* syntax in a syntax match. (There is no $[ .. ]+ syntax.)

The argument p is "auto-grouped", meaning that if the arity is greater than 1 it will be automatically replaced by group(p) to ensure that it produces exactly 1 value.

This parser has arity 1: it produces a nullKind node containing one argument for each invocation of p (or group(p)).

def Lean.Parser.ident : Parser

The parser ident parses a single identifier, possibly with namespaces, such as foo or bar.baz. The identifier must not be a declared token, so for example it will not match "def" because def is a keyword token. Tokens are implicitly declared by using them in string literals in parser declarations, so syntax foo := "bla" will make bla no longer legal as an identifier.

Identifiers can contain special characters or keywords if they are escaped using the «» characters: «def» is an identifier named def, and «x» is treated the same as x. This is useful for using disallowed characters in identifiers such as «foo.bar».baz or «hello world».

This parser has arity 1: it produces a Syntax.ident node containing the parsed identifier. You can use TSyntax.getId to extract the name from the resulting syntax object.

def Lean.Parser.identWithPartialTrailingDot : Parser

def Lean.Parser.rawIdent : Parser

def Lean.Parser.hygieneInfo : Parser

The parser hygieneInfo parses no text, but creates a hygieneInfoKind node containing an anonymous identifier as if it were parsed at the current position. This identifier is modified by syntax quotations to add macro scopes like a regular identifier.

This is used to implement have := ... syntax: the hygieneInfo between the have and := collects macro scopes, which we can apply to this when expanding to have this := .... See the language reference for more information about macro hygiene.

This is also used to implement cdot functions such as (1 + ·). The opening parenthesis contains a hygieneInfo node as does the cdot, which lets cdot expansion hygienically associate parentheses to cdots.

This parser has arity 1: it produces a hygieneInfoKind node containing an anonymous Syntax.ident. You can use HygieneInfo.mkIdent to create an Ident from the syntax object, but you can also use TSyntax.getHygieneInfo to get the raw name from the identifier.

def Lean.Parser.numLit : Parser

The parser num parses a numeric literal in several bases:

• Decimal: 129
• Hexadecimal: 0xdeadbeef
• Octal: 0o755
• Binary: 0b1101

This parser has arity 1: it produces a numLitKind node containing an atom with the text of the literal. You can use TSyntax.getNat to extract the number from the resulting syntax object.

def Lean.Parser.hexnum : Parser

The parser hexnum parses a hexadecimal numeric literal not containing the 0x prefix.

It produces a hexnumKind node containing an atom with the text of the literal. This parser is mainly used for creating atoms such #<hexnum>. Recall that hexnum is not a token and this parser must be prefixed by another parser.

For numerals such as 0xadef100a, you should use numLit.

def Lean.Parser.scientificLit : Parser

The parser scientific parses a scientific-notation literal, such as 1.3e-24.

This parser has arity 1: it produces a scientificLitKind node containing an atom with the text of the literal. You can use TSyntax.getScientific to extract the parts from the resulting syntax object.

def Lean.Parser.strLit : Parser

The parser str parses a string literal, such as "foo" or "\r\n". Strings can contain C-style escapes like \n, \", \x00 or \u2665, as well as literal unicode characters like ∈. Newlines in a string are interpreted literally.

This parser has arity 1: it produces a strLitKind node containing an atom with the raw literal (including the quote marks and without interpreting the escapes). You can use TSyntax.getString to decode the string from the resulting syntax object.

def Lean.Parser.charLit : Parser

The parser char parses a character literal, such as 'a' or '\n'. Character literals can contain C-style escapes like \n, \", \x00 or \u2665, as well as literal unicode characters like ∈, but must evaluate to a single unicode codepoint, so '♥' is allowed but '❤️' is not (since it is two codepoints but one grapheme cluster).

This parser has arity 1: it produces a charLitKind node containing an atom with the raw literal (including the quote marks and without interpreting the escapes). You can use TSyntax.getChar to decode the string from the resulting syntax object.

def Lean.Parser.nameLit : Parser

The parser name parses a name literal like `foo. The syntax is the same as for identifiers (see ident) but with a leading backquote.

This parser has arity 1: it produces a nameLitKind node containing the raw literal (including the backquote). You can use TSyntax.getName to extract the name from the resulting syntax object.

@[inline]

def Lean.Parser.group (p : Parser) : Parser

The parser group(p) parses the same thing as p, but it wraps the results in a groupKind node.

This parser always has arity 1, even if p does not. Parsers like p* are automatically rewritten to group(p)* if p does not have arity 1, so that the results from separate invocations of p can be differentiated.

@[inline]

def Lean.Parser.many1Indent (p : Parser) : Parser

The parser many1Indent(p) is equivalent to withPosition((colGe p)+). This has the effect of parsing one or more occurrences of p, where each subsequent p parse needs to be indented the same or more than the first parse.

This parser has arity 1, and returns a list of the results from p. p is "auto-grouped" if it is not arity 1.

@[inline]

def Lean.Parser.manyIndent (p : Parser) : Parser

The parser manyIndent(p) is equivalent to withPosition((colGe p)*). This has the effect of parsing zero or more occurrences of p, where each subsequent p parse needs to be indented the same or more than the first parse.

This parser has arity 1, and returns a list of the results from p. p is "auto-grouped" if it is not arity 1.

@[inline]

def Lean.Parser.sepByIndent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser

@[inline]

def Lean.Parser.sepBy1Indent (p : Parser) (sep : String) (psep : Parser := symbol sep) (allowTrailingSep : Bool := false) : Parser

def Lean.Parser.sepByIndent.formatter (p : PrettyPrinter.Formatter) (_sep : String) (pSep : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.Parser.sepBy1Indent.formatter (p : PrettyPrinter.Formatter) (_sep : String) (pSep : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

@[reducible, inline]

abbrev Lean.Parser.notSymbol (s : String) : Parser

@[inline]

def Lean.Parser.patternIgnore : Parser → Parser

No-op parser combinator that annotates subtrees to be ignored in syntax patterns.

@[inline]

def Lean.Parser.ppHardSpace : Parser

No-op parser that advises the pretty printer to emit a non-breaking space.

@[inline]

def Lean.Parser.ppSpace : Parser

No-op parser that advises the pretty printer to emit a space/soft line break.

@[inline]

def Lean.Parser.ppLine : Parser

No-op parser that advises the pretty printer to emit a hard line break.

@[inline]

def Lean.Parser.ppRealFill : Parser → Parser

No-op parser combinator that advises the pretty printer to emit a Format.fill node.

@[inline]

def Lean.Parser.ppRealGroup : Parser → Parser

No-op parser combinator that advises the pretty printer to emit a Format.group node.

@[inline]

def Lean.Parser.ppIndent : Parser → Parser

No-op parser combinator that advises the pretty printer to indent the given syntax without grouping it.

@[inline]

def Lean.Parser.ppGroup (p : Parser) : Parser

No-op parser combinator that advises the pretty printer to group and indent the given syntax. By default, only syntax categories are grouped.

@[inline]

def Lean.Parser.ppDedent : Parser → Parser

No-op parser combinator that advises the pretty printer to dedent the given syntax. Dedenting can in particular be used to counteract automatic indentation.

@[inline]

def Lean.Parser.ppAllowUngrouped : Parser

No-op parser combinator that allows the pretty printer to omit the group and indent operation in the enclosing category parser.

syntax ppAllowUngrouped "by " tacticSeq : term
-- allows a `by` after `:=` without linebreak in between:
theorem foo : True := by
  trivial

@[inline]

def Lean.Parser.ppDedentIfGrouped : Parser → Parser

No-op parser combinator that advises the pretty printer to dedent the given syntax, if it was grouped by the category parser. Dedenting can in particular be used to counteract automatic indentation.

@[inline]

def Lean.Parser.ppHardLineUnlessUngrouped : Parser

No-op parser combinator that prints a line break. The line break is soft if the combinator is followed by an ungrouped parser (see ppAllowUngrouped), otherwise hard.

def Lean.ppHardSpace.formatter : PrettyPrinter.Formatter

def Lean.ppSpace.formatter : PrettyPrinter.Formatter

def Lean.ppLine.formatter : PrettyPrinter.Formatter

def Lean.ppRealFill.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.ppRealGroup.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.ppIndent.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.ppDedent.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.ppAllowUngrouped.formatter : PrettyPrinter.Formatter

def Lean.ppDedentIfGrouped.formatter (p : PrettyPrinter.Formatter) : PrettyPrinter.Formatter

def Lean.ppHardLineUnlessUngrouped.formatter : PrettyPrinter.Formatter

def Lean.«termRegister_parser_alias(Kind:=_)______» : ParserDescr