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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• Lean.Parser.manyIndent p = Lean.Parser.withPosition (Lean.Parser.many (HAndThen.hAndThen (Lean.Parser.checkColGe "irrelevant") fun x => 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

@[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 = Lean.PrettyPrinter.Formatter.fill p

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

Equations

• Lean.ppRealGroup.formatter p = Lean.PrettyPrinter.Formatter.group p

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

Equations

• Lean.ppIndent.formatter p = Lean.PrettyPrinter.Formatter.indent p none

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

Equations

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

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

Equations

• Lean.ppAllowUngrouped.formatter = modify fun x => { stxTrav := x.stxTrav, leadWord := x.leadWord, isUngrouped := x.isUngrouped, mustBeGrouped := false, stack := x.stack }

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.