Documentation

Lean.Parser.Extra

source
def Lean.Parser.optional (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.many (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.many1 (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.ident:
Lean.Parser.Parser
Equations
source
def Lean.Parser.rawIdent:
Lean.Parser.Parser
Equations
source
def Lean.Parser.numLit:
Lean.Parser.Parser
Equations
source
def Lean.Parser.scientificLit:
Lean.Parser.Parser
Equations
source
def Lean.Parser.strLit:
Lean.Parser.Parser
Equations
source
def Lean.Parser.charLit:
Lean.Parser.Parser
Equations
source
def Lean.Parser.nameLit:
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.group (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.many1Indent (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.manyIndent (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
@[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.
source
@[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.
source
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.
source
def Lean.Parser.sepBy1Indent.formatter (p : Lean.PrettyPrinter.Formatter) (_sep : String) (pSep : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
source
@[inline]
abbrev Lean.Parser.notSymbol (s : String) :
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.ppHardSpace:
Lean.Parser.Parser

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

Equations
source
@[inline]
def Lean.Parser.ppSpace:
Lean.Parser.Parser

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

Equations
source
@[inline]
def Lean.Parser.ppLine:
Lean.Parser.Parser

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

Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
def Lean.ppHardSpace.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppSpace.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppLine.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppRealFill.formatter (p : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppRealGroup.formatter (p : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppIndent.formatter (p : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppDedent.formatter (p : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppAllowUngrouped.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.ppDedentIfGrouped.formatter (p : Lean.PrettyPrinter.Formatter) :
Lean.PrettyPrinter.Formatter
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.ppHardLineUnlessUngrouped.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.Parser.«termRegister_parser_alias(Kind:=_)____»:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.