@[inline]

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

@[inline]

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

def Lean.Parser.precedence : Parser

def Lean.Parser.optPrecedence : Parser

def Lean.Parser.Syntax.numPrec : Parser

def Lean.Parser.Syntax.paren : Parser

def Lean.Parser.Syntax.cat : Parser

def Lean.Parser.Syntax.unary : Parser

def Lean.Parser.Syntax.binary : Parser

def Lean.Parser.Syntax.sepBy : Parser

def Lean.Parser.Syntax.sepBy1 : Parser

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.

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.)

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.

def Lean.Parser.Command.namedName : Parser

def Lean.Parser.Command.optNamedName : Parser

def Lean.Parser.Command.identPrec : Parser

def Lean.Parser.Command.notationItem : Parser

def Lean.Parser.Command.prefix : Parser

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

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.

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.

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.

def Lean.Parser.Command.postfix : Parser

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

def Lean.Parser.Command.mixfixKind : Parser

def Lean.Parser.Command.mixfix : Parser

def Lean.Parser.Command.notation : Parser

def Lean.Parser.Command.optKind : Parser

def Lean.Parser.Command.macro_rules : Parser

def Lean.Parser.Command.syntax : Parser

def Lean.Parser.Command.syntaxAbbrev : Parser

def Lean.Parser.Command.catBehaviorBoth : Parser

def Lean.Parser.Command.catBehaviorSymbol : Parser

def Lean.Parser.Command.catBehavior : Parser

def Lean.Parser.Command.syntaxCat : Parser

def Lean.Parser.Command.macroArg : Parser

def Lean.Parser.Command.macroRhs : Parser

def Lean.Parser.Command.macroTail : Parser

def Lean.Parser.Command.macro : Parser

def Lean.Parser.Command.elab_rules : Parser

def Lean.Parser.Command.elabArg : Parser

def Lean.Parser.Command.elabTail : Parser

def Lean.Parser.Command.elab : Parser

def Lean.Parser.Command.binderPredicate : Parser

Declares a binder predicate. For example:

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