def Lean.Parser.optional (p : Lean.Parser.Parser) : Lean.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!)

Equations

• Lean.Parser.optional p = Lean.Parser.optionalNoAntiquot (Lean.Parser.withAntiquotSpliceAndSuffix `optional p (Lean.Parser.symbol "?"))

def Lean.Parser.many (p : Lean.Parser.Parser) : Lean.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)).

Equations

• Lean.Parser.many p = Lean.Parser.manyNoAntiquot (Lean.Parser.withAntiquotSpliceAndSuffix `many p (Lean.Parser.symbol "*"))

def Lean.Parser.many1 (p : Lean.Parser.Parser) : Lean.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)).

Equations

• Lean.Parser.many1 p = Lean.Parser.many1NoAntiquot (Lean.Parser.withAntiquotSpliceAndSuffix `many p (Lean.Parser.symbol "*"))

def Lean.Parser.ident : Lean.Parser.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.

Equations

• Lean.Parser.ident = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ident" Lean.identKind) Lean.Parser.identNoAntiquot

def Lean.Parser.identWithPartialTrailingDot : Lean.Parser.Parser

Equations

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

def Lean.Parser.rawIdent : Lean.Parser.Parser

Equations

• Lean.Parser.rawIdent = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ident" Lean.identKind) Lean.Parser.rawIdentNoAntiquot

def Lean.Parser.hygieneInfo : Lean.Parser.Parser

The parser hygieneInfo parses no text, but captures the current macro scope information as though it parsed an identifier at the current position. It returns a hygieneInfoKind node around an .ident which is Name.anonymous but with macro scopes like a regular identifier.

This is used to implement have := ... syntax: the hygieneInfo between the have and := substitutes for the identifier which would normally go there as in have x :=, so that we can expand have := to have this := while retaining the usual macro name resolution behavior. See doc/macro_overview.md for more information about macro hygiene.

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

Equations

• Lean.Parser.hygieneInfo = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "hygieneInfo" Lean.hygieneInfoKind false) Lean.Parser.hygieneInfoNoAntiquot

def Lean.Parser.numLit : Lean.Parser.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.

Equations

• Lean.Parser.numLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "num" Lean.numLitKind) Lean.Parser.numLitNoAntiquot

def Lean.Parser.scientificLit : Lean.Parser.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.

Equations

• Lean.Parser.scientificLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "scientific" Lean.scientificLitKind) Lean.Parser.scientificLitNoAntiquot

def Lean.Parser.strLit : Lean.Parser.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.

Equations

• Lean.Parser.strLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "str" Lean.strLitKind) Lean.Parser.strLitNoAntiquot

def Lean.Parser.charLit : Lean.Parser.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.

Equations

• Lean.Parser.charLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "char" Lean.charLitKind) Lean.Parser.charLitNoAntiquot

def Lean.Parser.nameLit : Lean.Parser.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.

Equations

• Lean.Parser.nameLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "name" Lean.nameLitKind) Lean.Parser.nameLitNoAntiquot

@[inline]

def Lean.Parser.group (p : Lean.Parser.Parser) : Lean.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.

Equations

• Lean.Parser.group p = Lean.Parser.node Lean.groupKind p

@[inline]

def Lean.Parser.many1Indent (p : Lean.Parser.Parser) : Lean.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.

Equations

• Lean.Parser.many1Indent p = Lean.Parser.withPosition (Lean.Parser.many1 (HAndThen.hAndThen (Lean.Parser.checkColGe "irrelevant") fun (x : Unit) => p))

@[inline]

def Lean.Parser.manyIndent (p : Lean.Parser.Parser) : Lean.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.

Equations

• Lean.Parser.manyIndent p = Lean.Parser.withPosition (Lean.Parser.many (HAndThen.hAndThen (Lean.Parser.checkColGe "irrelevant") fun (x : Unit) => p))

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

• Lean.Parser.sepBy1Indent.formatter = Lean.Parser.sepByIndent.formatter

@[reducible, inline]

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

Equations

• Lean.Parser.notSymbol s = Lean.Parser.notFollowedBy (Lean.Parser.symbol s) s

@[inline]

def Lean.Parser.patternIgnore : Lean.Parser.Parser → Lean.Parser.Parser

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

Equations

• Lean.Parser.patternIgnore = Lean.Parser.node `patternIgnore

@[inline]

def Lean.Parser.ppHardSpace : Lean.Parser.Parser

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

Equations

• Lean.Parser.ppHardSpace = Lean.Parser.skip

@[inline]

def Lean.Parser.ppSpace : Lean.Parser.Parser

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

Equations

• Lean.Parser.ppSpace = Lean.Parser.skip

@[inline]

def Lean.Parser.ppLine : Lean.Parser.Parser

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

Equations

• Lean.Parser.ppLine = Lean.Parser.skip

@[inline]

def Lean.Parser.ppRealFill : Lean.Parser.Parser → Lean.Parser.Parser

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

Equations

• Lean.Parser.ppRealFill = id

@[inline]

def Lean.Parser.ppRealGroup : Lean.Parser.Parser → Lean.Parser.Parser

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

Equations

• Lean.Parser.ppRealGroup = id

@[inline]

def Lean.Parser.ppIndent : Lean.Parser.Parser → Lean.Parser.Parser

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

Equations

• Lean.Parser.ppIndent = id

@[inline]

def Lean.Parser.ppGroup (p : Lean.Parser.Parser) : Lean.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.

Equations

• Lean.Parser.ppGroup p = Lean.Parser.ppRealFill (Lean.Parser.ppIndent p)

@[inline]

def Lean.Parser.ppDedent : Lean.Parser.Parser → Lean.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.

Equations

• Lean.Parser.ppDedent = id

@[inline]

def Lean.Parser.ppAllowUngrouped : Lean.Parser.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

Equations

• Lean.Parser.ppAllowUngrouped = Lean.Parser.skip

@[inline]

def Lean.Parser.ppDedentIfGrouped : Lean.Parser.Parser → Lean.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.

Equations

• Lean.Parser.ppDedentIfGrouped = id

@[inline]

def Lean.Parser.ppHardLineUnlessUngrouped : Lean.Parser.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.

Equations

• Lean.Parser.ppHardLineUnlessUngrouped = Lean.Parser.skip

def Lean.ppHardSpace.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.ppHardSpace.formatter = Lean.PrettyPrinter.Formatter.pushWhitespace (Std.Format.text " ")

def Lean.ppSpace.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.ppSpace.formatter = Lean.PrettyPrinter.Formatter.pushLine

def Lean.ppLine.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.ppLine.formatter = Lean.PrettyPrinter.Formatter.pushWhitespace (Std.Format.text "\n")

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

Equations

• Lean.ppRealFill.formatter p = p.fill

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

Equations

• Lean.ppRealGroup.formatter p = p.group

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

Equations

• Lean.ppIndent.formatter p = p.indent

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

Equations

• Lean.ppDedent.formatter p = do let opts ← Lean.getOptions p.indent (some (0 - ↑(Std.Format.getIndent opts)))

def Lean.ppAllowUngrouped.formatter : Lean.PrettyPrinter.Formatter

Equations

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

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

Equations

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

def Lean.ppHardLineUnlessUngrouped.formatter : Lean.PrettyPrinter.Formatter

Equations

• Lean.ppHardLineUnlessUngrouped.formatter = do let __do_lift ← get if __do_lift.isUngrouped = true then Lean.PrettyPrinter.Formatter.pushLine else Lean.ppLine.formatter

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

Equations

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