@[inline]

def Lean.Parser.precedenceParser (rbp : Nat := 0) : Parser

Equations

• Lean.Parser.precedenceParser rbp = Lean.Parser.categoryParser `prec rbp

@[inline]

def Lean.Parser.syntaxParser (rbp : Nat := 0) : Parser

Equations

• Lean.Parser.syntaxParser rbp = Lean.Parser.categoryParser `stx rbp

def Lean.Parser.precedence : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.optPrecedence : Parser

Equations

• Lean.Parser.optPrecedence = Lean.Parser.optional (Lean.Parser.atomic Lean.Parser.precedence)

def Lean.Parser.Syntax.numPrec : Parser

Equations

• Lean.Parser.Syntax.numPrec = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.numLit

def Lean.Parser.Syntax.paren : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.cat : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.unary : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.binary : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.sepBy : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.sepBy1 : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.atom : Parser

Parses the literal symbol.

The symbol is automatically included in the set of reserved tokens ("keywords"). Keywords cannot be used as identifiers, unless the identifier is otherwise escaped. For example, "fun" reserves fun as a keyword; to refer an identifier named fun one can write «fun». Adding a & prefix prevents it from being reserved, for example &"true".

Whitespace before or after the atom is used as a pretty printing hint. For example, " + " parses + and pretty prints it with whitespace on both sides. The whitespace has no effect on parsing behavior.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.nonReserved : Parser

Parses a literal symbol. The & prefix prevents it from being included in the set of reserved tokens ("keywords"). This means that the symbol can still be recognized as an identifier by other parsers.

Some syntax categories, such as tactic, automatically apply & to the first symbol.

Whitespace before or after the atom is used as a pretty printing hint. For example, " + " parses + and pretty prints it with whitespace on both sides. The whitespace has no effect on parsing behavior.

(Not exposed by parser description syntax: If the includeIdent argument is true, lets ident be reinterpreted as atom if it matches.)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.unicodeAtom : Parser

• unicode("→", "->") parses a symbol matching either → or ->. Each symbol is reserved. The second symbol is an ASCII version of the first. The pp.unicode option controls which is used when pretty printing.
• unicode("→", "->", preserveForPP) is the same except for pretty printing behavior. When the pp.unicode option is enabled, then the pretty printer uses whichever symbol matches the underlying atom in the syntax. The intent is that preserveForPP means that the ASCII variant is preferred. For example, fun notation uses preserveForPP for its arrow; the delaborator chooses ↦ or => depending on the value of pp.unicode.fun, letting users opt-in to formatting with ↦. Note that notation creates a pretty printer preferring the ASCII version.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.namedName : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.optNamedName : Parser

Equations

• Lean.Parser.Command.optNamedName = Lean.Parser.optional Lean.Parser.Command.namedName

def Lean.Parser.Command.identPrec : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.notationItem : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.prefix : Parser

prefix:prec "op" => f is equivalent to notation:prec "op" x:prec => f x.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infix : Parser

infix:prec "op" => f is equivalent to notation:prec x:prec1 "op" y:prec1 => f x y, where prec1 := prec + 1.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infixl : Parser

infixl:prec "op" => f is equivalent to notation:prec x:prec "op" y:prec1 => f x y, where prec1 := prec + 1.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infixr : Parser

infixr:prec "op" => f is equivalent to notation:prec x:prec1 "op" y:prec => f x y, where prec1 := prec + 1.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.postfix : Parser

postfix:prec "op" => f is equivalent to notation:prec x:prec "op" => f x.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.mixfixKind : Parser

Equations

• Lean.Parser.Command.mixfixKind = (Lean.Parser.Command.prefix <|> Lean.Parser.Command.infix <|> Lean.Parser.Command.infixl <|> Lean.Parser.Command.infixr <|> Lean.Parser.Command.postfix)

def Lean.Parser.Command.mixfix : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.notation : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.optKind : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macro_rules : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntax : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntaxAbbrev : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehaviorBoth : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehaviorSymbol : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehavior : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntaxCat : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroArg : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroRhs : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroTail : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macro : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elab_rules : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elabArg : Parser

Equations

• Lean.Parser.Command.elabArg = Lean.Parser.Command.macroArg

def Lean.Parser.Command.elabTail : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elab : Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.binderPredicate : Parser

Declares a binder predicate. For example:

binder_predicate x " > " y:term => `($x > $y)

Equations

• One or more equations did not get rendered due to their size.