def Lean.Parser.Command.commentBody : Lean.Parser.Parser

def Lean.Parser.Command.commentBody.parenthesizer : Lean.PrettyPrinter.Parenthesizer

def Lean.Parser.Command.commentBody.formatter : Lean.PrettyPrinter.Formatter

def Lean.Parser.Command.docComment : Lean.Parser.Parser

@[inline]

def Lean.Parser.tacticParser (rbp : optParam Nat 0) : Lean.Parser.Parser

@[inline]

def Lean.Parser.convParser (rbp : optParam Nat 0) : Lean.Parser.Parser

def Lean.Parser.Tactic.sepByIndentSemicolon (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.Tactic.sepBy1IndentSemicolon (p : Lean.Parser.Parser) : Lean.Parser.Parser

def Lean.Parser.Tactic.tacticSeq1Indented : Lean.Parser.Parser

def Lean.Parser.Tactic.tacticSeqBracketed : Lean.Parser.Parser

The syntax { tacs } is an alternative syntax for · tacs. It runs the tactics in sequence, and fails if the goal is not solved.

def Lean.Parser.Tactic.tacticSeq : Lean.Parser.Parser

A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the first tactic of the sequence.

def Lean.Parser.Tactic.tacticSeqIndentGt : Lean.Parser.Parser

Same as [tacticSeq] but requires delimiter-free tactic sequence to have strict indentation. The strict indentation requirement only apply to nested bys, as top-level bys do not have a position set.

def Lean.Parser.Tactic.seq1 : Lean.Parser.Parser

def Lean.Parser.darrow : Lean.Parser.Parser

def Lean.Parser.semicolonOrLinebreak : Lean.Parser.Parser

Built-in parsers

def Lean.Parser.Term.byTactic : Lean.Parser.Parser

by tac constructs a term of the expected type by running the tactic(s) tac.

def Lean.Parser.Term.byTactic' : Lean.Parser.Parser

def Lean.Parser.Term.optSemicolon (p : Lean.Parser.Parser) : Lean.Parser.Parser

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

def Lean.Parser.Term.num : Lean.Parser.Parser

def Lean.Parser.Term.scientific : Lean.Parser.Parser

def Lean.Parser.Term.str : Lean.Parser.Parser

def Lean.Parser.Term.char : Lean.Parser.Parser

def Lean.Parser.Term.type : Lean.Parser.Parser

A type universe. Type ≡ Type 0, Type u ≡ Sort (u + 1).

def Lean.Parser.Term.sort : Lean.Parser.Parser

A specific universe in Lean's infinite hierarchy of universes.

def Lean.Parser.Term.prop : Lean.Parser.Parser

The universe of propositions. Prop ≡ Sort 0.

def Lean.Parser.Term.hole : Lean.Parser.Parser

A placeholder term, to be synthesized by unification.

def Lean.Parser.Term.syntheticHole : Lean.Parser.Parser

def Lean.Parser.Term.binderIdent : Lean.Parser.Parser

def Lean.Parser.Term.sorry : Lean.Parser.Parser

A temporary placeholder for a missing proof or value.

def Lean.Parser.Term.cdot : Lean.Parser.Parser

A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses. For example, (· + ·) is equivalent to fun x y => x + y.

def Lean.Parser.Term.typeAscription : Lean.Parser.Parser

Type ascription notation: (0 : Int) instructs Lean to process 0 as a value of type Int. An empty type ascription (e :) elaborates e without the expected type. This is occasionally useful when Lean's heuristics for filling arguments from the expected type do not yield the right result.

def Lean.Parser.Term.tuple : Lean.Parser.Parser

Tuple notation; () is short for Unit.unit, (a, b, c) for Prod.mk a (Prod.mk b c), etc.

def Lean.Parser.Term.paren : Lean.Parser.Parser

Parentheses, used for grouping expressions (e.g., a * (b + c)). Can also be used for creating simple functions when combined with ·. Here are some examples:

• (· + 1) is shorthand for fun x => x + 1
• (· + ·) is shorthand for fun x y => x + y
• (f · a b) is shorthand for fun x => f x a b
• (h (· + 1) ·) is shorthand for fun x => h (fun y => y + 1) x
• also applies to other parentheses-like notations such as (·, 1)

def Lean.Parser.Term.anonymousCtor : Lean.Parser.Parser

The anonymous constructor ⟨e, ...⟩ is equivalent to c e ... if the expected type is an inductive type with a single constructor c. If more terms are given than c has parameters, the remaining arguments are turned into a new anonymous constructor application. For example, ⟨a, b, c⟩ : α × (β × γ) is equivalent to ⟨a, ⟨b, c⟩⟩.

def Lean.Parser.Term.optIdent : Lean.Parser.Parser

def Lean.Parser.Term.fromTerm : Lean.Parser.Parser

def Lean.Parser.Term.showRhs : Lean.Parser.Parser

def Lean.Parser.Term.sufficesDecl : Lean.Parser.Parser

def Lean.Parser.Term.suffices : Lean.Parser.Parser

def Lean.Parser.Term.show : Lean.Parser.Parser

def Lean.Parser.Term.structInstArrayRef : Lean.Parser.Parser

def Lean.Parser.Term.structInstLVal : Lean.Parser.Parser

def Lean.Parser.Term.structInstField : Lean.Parser.Parser

def Lean.Parser.Term.structInstFieldAbbrev : Lean.Parser.Parser

def Lean.Parser.Term.optEllipsis : Lean.Parser.Parser

def Lean.Parser.Term.structInst : Lean.Parser.Parser

Structure instance. { x := e, ... } assigns e to field x, which may be inherited. If e is itself a variable called x, it can be elided: fun y => { x := 1, y }. A structure update of an existing value can be given via with: { point with x := 1 }. The structure type can be specified if not inferable: { x := 1, y := 2 : Point }.

def Lean.Parser.Term.typeSpec : Lean.Parser.Parser

def Lean.Parser.Term.optType : Lean.Parser.Parser

def Lean.Parser.Term.explicit : Lean.Parser.Parser

@x disables automatic insertion of implicit parameters of the constant x. @e for any term e also disables the insertion of implicit lambdas at this position.

def Lean.Parser.Term.inaccessible : Lean.Parser.Parser

.(e) marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking. In contrast to regular patterns, e may be an arbitrary term of the appropriate type.

def Lean.Parser.Term.binderType (requireType : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.Term.binderTactic : Lean.Parser.Parser

def Lean.Parser.Term.binderDefault : Lean.Parser.Parser

def Lean.Parser.Term.binderDefault.parenthesizer : Lean.PrettyPrinter.Parenthesizer

def Lean.Parser.Term.explicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.Term.implicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

Implicit binder. In regular applications without @, it is automatically inserted and solved by unification whenever all explicit parameters before it are specified.

def Lean.Parser.Term.strictImplicitLeftBracket : Lean.Parser.Parser

def Lean.Parser.Term.strictImplicitRightBracket : Lean.Parser.Parser

def Lean.Parser.Term.strictImplicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

Strict-implicit binder. In contrast to { ... } regular implicit binders, a strict-implicit binder is inserted automatically only when at least one subsequent explicit parameter is specified.

def Lean.Parser.Term.instBinder : Lean.Parser.Parser

Instance-implicit binder. In regular applications without @, it is automatically inserted and solved by typeclass inference of the specified class.

def Lean.Parser.Term.bracketedBinder (requireType : optParam Bool false) : Lean.Parser.Parser

def Lean.Parser.Term.depArrow : Lean.Parser.Parser

def Lean.Parser.Term.forall : Lean.Parser.Parser

def Lean.Parser.Term.matchAlt (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) : Lean.Parser.Parser

def Lean.Parser.Term.matchAltExpr : Lean.Parser.Parser

Useful for syntax quotations. Note that generic patterns such as `(matchAltExpr| | ... => $rhs) should also work with other rhsParsers (of arity 1).

instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe (Lean.TSyntax `Lean.Parser.Term.matchAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchAlt)

def Lean.Parser.Term.matchAlts (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) : Lean.Parser.Parser

def Lean.Parser.Term.matchDiscr : Lean.Parser.Parser

def Lean.Parser.Term.trueVal : Lean.Parser.Parser

def Lean.Parser.Term.falseVal : Lean.Parser.Parser

def Lean.Parser.Term.generalizingParam : Lean.Parser.Parser

def Lean.Parser.Term.motive : Lean.Parser.Parser

def Lean.Parser.Term.match : Lean.Parser.Parser

Pattern matching. match e, ... with | p, ... => f | ... matches each given term e against each pattern p of a match alternative. When all patterns of an alternative match, the match term evaluates to the value of the corresponding right-hand side f with the pattern variables bound to the respective matched values. When not constructing a proof, match does not automatically substitute variables matched on in dependent variables' types. Use match (generalizing := true) ... to enforce this.

Syntax quotations can also be used in a pattern match. This matches a Syntax value against quotations, pattern variables, or _.

Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly.

Syntax.atoms are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in

syntax "c" ("foo" <|> "bar") ...

foo and bar are indistinguishable during matching, but in

syntax foo := "foo"
syntax "c" (foo <|> "bar") ...

they are not.

def Lean.Parser.Term.nomatch : Lean.Parser.Parser

Empty match/ex falso. nomatch e is of arbitrary type α : Sort u if Lean can show that an empty set of patterns is exhaustive given e's type, e.g. because it has no constructors.

def Lean.Parser.Term.funImplicitBinder : Lean.Parser.Parser

def Lean.Parser.Term.funStrictImplicitBinder : Lean.Parser.Parser

def Lean.Parser.Term.funBinder : Lean.Parser.Parser

def Lean.Parser.Term.basicFun : Lean.Parser.Parser

def Lean.Parser.Term.fun : Lean.Parser.Parser

def Lean.Parser.Term.optExprPrecedence : Lean.Parser.Parser

def Lean.Parser.Term.withAnonymousAntiquot : Lean.Parser.Parser

def Lean.Parser.Term.leading_parser : Lean.Parser.Parser

def Lean.Parser.Term.trailing_parser : Lean.Parser.Parser

def Lean.Parser.Term.borrowed : Lean.Parser.Parser

def Lean.Parser.Term.quotedName : Lean.Parser.Parser

A literal of type Name.

def Lean.Parser.Term.doubleQuotedName : Lean.Parser.Parser

A resolved name literal. Evaluates to the full name of the given constant if existent in the current context, or else fails.

def Lean.Parser.Term.letIdBinder : Lean.Parser.Parser

def Lean.Parser.Term.letIdLhs : Lean.Parser.Parser

def Lean.Parser.Term.letIdDecl : Lean.Parser.Parser

def Lean.Parser.Term.letPatDecl : Lean.Parser.Parser

def Lean.Parser.Term.letEqnsDecl : Lean.Parser.Parser

def Lean.Parser.Term.letDecl : Lean.Parser.Parser

def Lean.Parser.Term.let : Lean.Parser.Parser

let is used to declare a local definition. Example:

let x := 1
let y := x + 1
x + y

Since functions are first class citizens in Lean, you can use let to declare local functions too.

let double := fun x => 2*x
double (double 3)

For recursive definitions, you should use let rec. You can also perform pattern matching using let. For example, assume p has type Nat × Nat, then you can write

let (x, y) := p
x + y

def Lean.Parser.Term.let_fun : Lean.Parser.Parser

let_fun x := v; b is syntax sugar for (fun x => b) v. It is very similar to let x := v; b, but they are not equivalent. In let_fun, the value v has been abstracted away and cannot be accessed in b.

def Lean.Parser.Term.let_delayed : Lean.Parser.Parser

let_delayed x := v; b is similar to let x := v; b, but b is elaborated before v.

def Lean.Parser.Term.let_tmp : Lean.Parser.Parser

let-declaration that is only included in the elaborated term if variable is still there. It is often used when building macros.

def Lean.Parser.Term.haveIdLhs : Lean.Parser.Parser

def Lean.Parser.Term.haveIdDecl : Lean.Parser.Parser

def Lean.Parser.Term.haveEqnsDecl : Lean.Parser.Parser

def Lean.Parser.Term.haveDecl : Lean.Parser.Parser

def Lean.Parser.Term.have : Lean.Parser.Parser

def Lean.Parser.Term.scoped : Lean.Parser.Parser

def Lean.Parser.Term.local : Lean.Parser.Parser

def Lean.Parser.Term.attrKind : Lean.Parser.Parser

def Lean.Parser.Term.attrInstance : Lean.Parser.Parser

def Lean.Parser.Term.attributes : Lean.Parser.Parser

def Lean.Parser.Term.letRecDecl : Lean.Parser.Parser

def Lean.Parser.Term.letRecDecls : Lean.Parser.Parser

def Lean.Parser.Term.letrec : Lean.Parser.Parser

def Lean.Parser.Term.whereDecls : Lean.Parser.Parser

def Lean.Parser.Term.matchAltsWhereDecls : Lean.Parser.Parser

def Lean.Parser.Term.noindex : Lean.Parser.Parser

def Lean.Parser.Term.binrel : Lean.Parser.Parser

def Lean.Parser.Term.binrel_no_prop : Lean.Parser.Parser

Similar to binrel, but coerce Prop arguments into Bool.

def Lean.Parser.Term.binop : Lean.Parser.Parser

def Lean.Parser.Term.binop_lazy : Lean.Parser.Parser

def Lean.Parser.Term.unop : Lean.Parser.Parser

def Lean.Parser.Term.forInMacro : Lean.Parser.Parser

def Lean.Parser.Term.forInMacro' : Lean.Parser.Parser

def Lean.Parser.Term.declName : Lean.Parser.Parser

A macro which evaluates to the name of the currently elaborating declaration.

def Lean.Parser.Term.withDeclName : Lean.Parser.Parser

• with_decl_name% id e elaborates e in a context while changing the effective declaration name to id.
• with_decl_name% ?id e does the same, but resolves id as a new definition name (appending the current namespaces).

def Lean.Parser.Term.typeOf : Lean.Parser.Parser

def Lean.Parser.Term.ensureTypeOf : Lean.Parser.Parser

def Lean.Parser.Term.ensureExpectedType : Lean.Parser.Parser

def Lean.Parser.Term.noImplicitLambda : Lean.Parser.Parser

def Lean.Parser.Term.clear : Lean.Parser.Parser

clear% x; e elaborates x after clearing the free variable x from the local context. If x cannot be cleared (due to dependencies), it will keep x without failing.

def Lean.Parser.Term.letMVar : Lean.Parser.Parser

def Lean.Parser.Term.waitIfTypeMVar : Lean.Parser.Parser

def Lean.Parser.Term.waitIfTypeContainsMVar : Lean.Parser.Parser

def Lean.Parser.Term.waitIfContainsMVar : Lean.Parser.Parser

def Lean.Parser.Term.defaultOrOfNonempty : Lean.Parser.Parser

def Lean.Parser.Term.noErrorIfUnused : Lean.Parser.Parser

Helper parser for marking match-alternatives that should not trigger errors if unused. We use them to implement macro_rules and elab_rules

def Lean.Parser.Term.namedArgument : Lean.Parser.Parser

def Lean.Parser.Term.ellipsis : Lean.Parser.Parser

def Lean.Parser.Term.argument : Lean.Parser.Parser

def Lean.Parser.Term.app : Lean.Parser.TrailingParser

def Lean.Parser.Term.proj : Lean.Parser.TrailingParser

The extended field notation e.f is roughly short for T.f e where T is the type of e. More precisely,

• if e is of a function type, e.f is translated to Function.f (p := e) where p is the first explicit parameter of function type
• if e is of a named type T ... and there is a declaration T.f (possibly from export), e.f is translated to T.f (p := e) where p is the first explicit parameter of type T ...
• otherwise, if e is of a structure type, the above is repeated for every base type of the structure.

The field index notation e.i, where i is a positive number, is short for accessing the i-th field (1-indexed) of e if it is of a structure type.

def Lean.Parser.Term.completion : Lean.Parser.TrailingParser

def Lean.Parser.Term.arrow : Lean.Parser.TrailingParser

def Lean.Parser.Term.isIdent (stx : Lean.Syntax) : Bool

def Lean.Parser.Term.explicitUniv : Lean.Parser.TrailingParser

x.{u, ...} explicitly specifies the universes u, ... of the constant x.

def Lean.Parser.Term.namedPattern : Lean.Parser.TrailingParser

x@e matches the pattern e and binds its value to the identifier x.

def Lean.Parser.Term.pipeProj : Lean.Parser.TrailingParser

e |>.x is a shorthand for (e).x. It is especially useful for avoiding parentheses with repeated applications.

def Lean.Parser.Term.pipeCompletion : Lean.Parser.TrailingParser

def Lean.Parser.Term.subst : Lean.Parser.TrailingParser

h ▸ e is a macro built on top of Eq.rec and Eq.symm definitions. Given h : a = b and e : p a, the term h ▸ e has type p b. You can also view h ▸ e as a "type casting" operation where you change the type of e by using h. See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.

def Lean.Parser.Term.bracketedBinderF : Lean.Parser.Parser

instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_1 : Coe (Lean.TSyntax `Lean.Parser.Term.bracketedBinderF) (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

def Lean.Parser.Term.panic : Lean.Parser.Parser

panic! msg formally evaluates to @Inhabited.default α if the expected type α implements Inhabited. At runtime, msg and the file position are printed to stderr unless the C function lean_set_panic_messages(false) has been executed before. If the C function lean_set_exit_on_panic(true) has been executed before, the process is then aborted.

def Lean.Parser.Term.unreachable : Lean.Parser.Parser

A shorthand for panic! "unreachable code has been reached".

def Lean.Parser.Term.dbgTrace : Lean.Parser.Parser

dbg_trace e; body evaluates to body and prints e (which can be an interpolated string literal) to stderr. It should only be used for debugging.

def Lean.Parser.Term.assert : Lean.Parser.Parser

assert! cond panics if cond evaluates to false.

def Lean.Parser.Term.macroArg : Lean.Parser.Parser

def Lean.Parser.Term.macroDollarArg : Lean.Parser.Parser

def Lean.Parser.Term.macroLastArg : Lean.Parser.Parser

def Lean.Parser.Term.stateRefT : Lean.Parser.Parser

def Lean.Parser.Term.dynamicQuot : Lean.Parser.Parser

def Lean.Parser.Term.dotIdent : Lean.Parser.Parser

def Lean.Parser.Tactic.quot : Lean.Parser.Parser

def Lean.Parser.Tactic.quotSeq : Lean.Parser.Parser