# Documentation

Lean.Parser.Term

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

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

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

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.

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

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.

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

# Built-in parsers #

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

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

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

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

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

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

The universe of propositions. Prop ≡ Sort 0≡ Sort 0.

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

A placeholder term, to be synthesized by unification.

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

A temporary placeholder for a missing proof or value.

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

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.

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

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.

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

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

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

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)
Equations
• One or more equations did not get rendered due to their size.

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

Equations
instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil :
Coe (Lean.TSyntax Lean.Parser.Term.matchAltExpr) (Lean.TSyntax Lean.Parser.Term.matchAlt)
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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.

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

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.

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

A literal of type Name.

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

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

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

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× Nat, then you can write

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

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

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.

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

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

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

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

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

Similar to binrel, but coerce Prop arguments into Bool.

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

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

Equations
• One or more equations did not get rendered due to their size.
• 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).
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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.

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

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

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

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.

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

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

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

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

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

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

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

h ▸ e▸ 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▸ e has type p b. You can also view h ▸ e▸ 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.

Equations
• One or more equations did not get rendered due to their size.
Equations
instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_1 :
Coe (Lean.TSyntax Lean.Parser.Term.bracketedBinderF) (Lean.TSyntax Lean.Parser.Term.bracketedBinder)
Equations

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.

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

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

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

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.

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

assert! cond panics if cond evaluates to false`.

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