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

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

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

def Lean.Parser.ident : Lean.Parser.Parser

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

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

def Lean.Parser.numLit : Lean.Parser.Parser

def Lean.Parser.scientificLit : Lean.Parser.Parser

def Lean.Parser.strLit : Lean.Parser.Parser

def Lean.Parser.charLit : Lean.Parser.Parser

def Lean.Parser.nameLit : Lean.Parser.Parser

@[inline]

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

@[inline]

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

@[inline]

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

@[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

@[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

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

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

@[inline, reducible]

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[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.

@[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.

@[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.

@[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.

@[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.

@[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

@[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.

@[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.

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

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

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

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

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

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

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

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

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

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

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