Documentation

Lean.Parser.Extra

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
Instances For

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
Instances For

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
Instances For

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
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For

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
Instances For

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
Instances For

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
Instances For

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
Instances For

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
Instances For

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
Instances For
@[inline]

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
Instances For
@[inline]

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
Instances For
@[inline]

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
Instances For
@[inline]
def Lean.Parser.sepByIndent (p : Lean.Parser.Parser) (sep : String) (psep : ) (allowTrailingSep : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Parser.sepBy1Indent (p : Lean.Parser.Parser) (sep : String) (psep : ) (allowTrailingSep : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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

Equations
Instances For
@[inline]

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
Instances For
@[inline]

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
Instances For
@[inline]

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
Instances For
@[inline]

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
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• = p.fill
Instances For
Equations
• = p.group
Instances For
Equations
• = p.indent
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For