Documentation

Lean.Parser.Extra

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" (some Lean.identKind)) Lean.Parser.identNoAntiquot

def Lean.Parser.rawIdent :

Lean.Parser.Parser

Equations

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

def Lean.Parser.numLit :

Lean.Parser.Parser

Equations

Lean.Parser.numLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "numLit" (some Lean.numLitKind)) Lean.Parser.numLitNoAntiquot

def Lean.Parser.scientificLit :

Lean.Parser.Parser

Equations

Lean.Parser.scientificLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "scientificLit" (some Lean.scientificLitKind)) Lean.Parser.scientificLitNoAntiquot

def Lean.Parser.strLit :

Lean.Parser.Parser

Equations

Lean.Parser.strLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "strLit" (some Lean.strLitKind)) Lean.Parser.strLitNoAntiquot

def Lean.Parser.charLit :

Lean.Parser.Parser

Equations

Lean.Parser.charLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "charLit" (some Lean.charLitKind)) Lean.Parser.charLitNoAntiquot

def Lean.Parser.nameLit :

Lean.Parser.Parser

Equations

Lean.Parser.nameLit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "nameLit" (some Lean.nameLitKind)) 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]

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.ppHardSpace :

Lean.Parser.Parser

Equations

Lean.Parser.ppHardSpace = Lean.Parser.skip

@[inline]

def Lean.Parser.ppSpace :

Lean.Parser.Parser

Equations

Lean.Parser.ppSpace = Lean.Parser.skip

@[inline]

def Lean.Parser.ppLine :

Lean.Parser.Parser

Equations

Lean.Parser.ppLine = Lean.Parser.skip

@[inline]

def Lean.Parser.ppRealFill :

Lean.Parser.Parser → Lean.Parser.Parser

Equations

Lean.Parser.ppRealFill = id

@[inline]

def Lean.Parser.ppRealGroup :

Lean.Parser.Parser → Lean.Parser.Parser

Equations

Lean.Parser.ppRealGroup = id

@[inline]

def Lean.Parser.ppIndent :

Lean.Parser.Parser → Lean.Parser.Parser

Equations

Lean.Parser.ppIndent = id

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.ppGroup p = Lean.Parser.ppRealFill (Lean.Parser.ppIndent p)

@[inline]

def Lean.Parser.ppDedent :

Lean.Parser.Parser → Lean.Parser.Parser

Equations

Lean.Parser.ppDedent = id

@[inline]

def Lean.Parser.ppAllowUngrouped :

Lean.Parser.Parser

Equations

Lean.Parser.ppAllowUngrouped = Lean.Parser.skip

@[inline]

def Lean.Parser.ppDedentIfGrouped :

Lean.Parser.Parser → Lean.Parser.Parser

Equations

Lean.Parser.ppDedentIfGrouped = id

@[inline]

def Lean.Parser.ppHardLineUnlessUngrouped :

Lean.Parser.Parser

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 a => { stxTrav := a.stxTrav, leadWord := a.leadWord, isUngrouped := a.isUngrouped, mustBeGrouped := false, stack := a.stack }

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

Lean.PrettyPrinter.Formatter

Equations

Lean.ppDedentIfGrouped.formatter p = do Lean.PrettyPrinter.Formatter.concat p let a ← Lean.getOptions let indent : Nat := Std.Format.getIndent a let a ← get if a.isUngrouped = true then pure PUnit.unit else modify fun st => { stxTrav := st.stxTrav, leadWord := st.leadWord, isUngrouped := st.isUngrouped, mustBeGrouped := st.mustBeGrouped, stack := Array.modify st.stack (Array.size st.stack - 1) fun a => Lean.Format.nest (0 - Int.ofNat indent) a }

def Lean.ppHardLineUnlessUngrouped.formatter :

Lean.PrettyPrinter.Formatter

Equations

Lean.ppHardLineUnlessUngrouped.formatter = do let a ← get if a.isUngrouped = true then Lean.PrettyPrinter.Formatter.pushLine else Lean.ppLine.formatter

def Lean.Parser.termRegister_parser_alias___ :

Lean.ParserDescr

Equations

Lean.Parser.termRegister_parser_alias___ = Lean.ParserDescr.node `Lean.Parser.termRegister_parser_alias___ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "register_parser_alias") (Lean.ParserDescr.unary `optional (Lean.ParserDescr.parser `Lean.Parser.strLit))) (Lean.ParserDescr.parser `Lean.Parser.ident))