# Documentation

Lean.Parser.Extra

Equations
Equations
Equations
@[inline]
Equations
@[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.
@[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.
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
@[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
@[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
@[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
@[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
@[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
Equations
• = do let opts ← Lean.getOptions
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.