## Equations

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

## Instances For

A `docComment`

parses a "documentation comment" like `/-- foo -/`

. This is not treated like
a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

A `docComment`

node contains a `/--`

atom and then the remainder of the comment, `foo -/`

in this
example. Use `TSyntax.getDocString`

to extract the body text from a doc string syntax node.

## Equations

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

## Instances For

## Equations

- Lean.Parser.tacticParser rbp = Lean.Parser.categoryParser `tactic rbp

## Instances For

`sepByIndentSemicolon(p)`

parses a sequence of `p`

optionally followed by `;`

,
similar to `manyIndent(p ";"?)`

, except that if two occurrences of `p`

occur on the same line,
the `;`

is mandatory. This is used by tactic parsing, so that

```
example := by
skip
skip
```

is legal, but `by skip skip`

is not - it must be written as `by skip; skip`

.

## Equations

## Instances For

`sepBy1IndentSemicolon(p)`

parses a (nonempty) sequence of `p`

optionally followed by `;`

,
similar to `many1Indent(p ";"?)`

, except that if two occurrences of `p`

occur on the same line,
the `;`

is mandatory. This is used by tactic parsing, so that

```
example := by
skip
skip
```

is legal, but `by skip skip`

is not - it must be written as `by skip; skip`

.

## Equations

## Instances For

## Equations

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

## Instances For

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.

## Instances For

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.

## Instances For

Same as [`tacticSeq`

] but requires delimiter-free tactic sequence to have strict indentation.
The strict indentation requirement only apply to *nested* `by`

s, as top-level `by`

s do not have a
position set.

## Equations

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

## Instances For

## Equations

- Lean.Parser.Tactic.seq1 = Lean.Parser.node `Lean.Parser.Tactic.seq1 (Lean.Parser.sepBy1 Lean.Parser.tacticParser ";\n" (Lean.Parser.symbol ";\n") true)

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Instances For

## Equations

## Instances For

A type universe. `Type ≡ Type 0`

, `Type u ≡ Sort (u + 1)`

.

## Equations

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

## Instances For

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

## Equations

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

## Instances For

The universe of propositions. `Prop ≡ Sort 0`

.

## Equations

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

## Instances For

A placeholder term, to be synthesized by unification.

## Equations

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

## Instances For

Parses a "synthetic hole", that is, `?foo`

or `?_`

.
This syntax is used to construct named metavariables.

## Equations

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

## Instances For

The `⋯`

term denotes a term that was omitted by the pretty printer.
The presence of `⋯`

in pretty printer output is controlled by the `pp.deepTerms`

and `pp.proofs`

options,
and these options can be further adjusted using `pp.deepTerms.threshold`

and `pp.proofs.threshold`

.

It is only meant to be used for pretty printing.
However, in case it is copied and pasted from the Infoview, `⋯`

logs a warning and elaborates like `_`

.

## Equations

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

## Instances For

## Equations

## Instances For

A temporary placeholder for a missing proof or value.

## Equations

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

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

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.

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

A `sufficesDecl`

represents everything that comes after the `suffices`

keyword:
an optional `x :`

, then a term `ty`

, then `from val`

or `by tac`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Instances For

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

## Instances For

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Explicit binder, like `(x y : A)`

or `(x y)`

.
Default values can be specified using `(x : A := v)`

syntax, and tactics using `(x : A := by tac)`

.

## Equations

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

## Instances For

Implicit binder, like `{x y : A}`

or `{x y}`

.
In regular applications, whenever all parameters before it have been specified,
then a `_`

placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.

In `@`

explicit mode, implicit binders behave like explicit binders.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Strict-implicit binder, like `⦃x y : A⦄`

or `⦃x y⦄`

.
In contrast to `{ ... }`

implicit binders, strict-implicit binders do not automatically insert
a `_`

placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.

Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x`

and `hs : y ∈ s`

,
then `h`

by itself elaborates to itself without inserting `_`

for the `x : A`

parameter,
and `h hs`

has type `p y`

.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`

, then `h`

by itself elaborates to have type `?m ∈ s → p ?m`

with `?m`

a fresh metavariable.

## Equations

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

## Instances For

Instance-implicit binder, like `[C]`

or `[inst : C]`

.
In regular applications without `@`

explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`

.
In `@`

explicit mode, if `_`

is used for an an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)`

to inhibit this and have it be solved for by unification instead, like an implicit argument.

## Equations

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

## Instances For

A `bracketedBinder`

matches any kind of binder group that uses some kind of brackets:

- An explicit binder like
`(x y : A)`

- An implicit binder like
`{x y : A}`

- A strict implicit binder,
`⦃y z : A⦄`

or its ASCII alternative`{{y z : A}}`

- An instance binder
`[A]`

or`[x : A]`

(multiple variables are not allowed here)

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Useful for syntax quotations. Note that generic patterns such as ``(matchAltExpr| | ... => $rhs)`

should also
work with other `rhsParser`

s (of arity 1).

## Equations

- Lean.Parser.Term.matchAltExpr = Lean.Parser.Term.matchAlt

## Instances For

## Equations

- Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean = { coe := fun (stx : Lean.TSyntax `Lean.Parser.Term.matchAltExpr) => { raw := stx.raw } }

## Equations

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

## Instances For

`matchDiscr`

matches a "match discriminant", either `h : tm`

or `tm`

, used in `match`

as
`match h1 : e1, e2, h3 : e3 with ...`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.
If used as `match h : e, ... with | p, ... => f | ...`

, `h : e = p`

is available
within `f`

.

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.atom`

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

A literal of type `Name`

.

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

`letDecl`

matches the body of a let declaration `let f x1 x2 := e`

,
`let pat := e`

(where `pat`

is an arbitrary term) or `let f | pat1 => e1 | pat2 => e2 ...`

(a pattern matching declaration), except for the `let`

keyword itself.
`let rec`

declarations are not handled here.

## Equations

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

## Instances For

`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
```

## Equations

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

## Instances For

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

## Instances For

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

`haveDecl`

matches the body of a have declaration: `have := e`

, `have f x1 x2 := e`

,
`have pat := e`

(where `pat`

is an arbitrary term) or `have f | pat1 => e1 | pat2 => e2 ...`

(a pattern matching declaration), except for the `have`

keyword itself.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

`attrKind`

matches `("scoped" <|> "local")?`

, used before an attribute like `@[local simp]`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Specify a termination argument for well-founded termination:

```
termination_by a - b
```

indicates that termination of the currently defined recursive function follows
because the difference between the the arguments `a`

and `b`

.

If the fuction takes further argument after the colon, you can name them as follows:

```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```

If omitted, a termination argument will be inferred. If written as `termination_by?`

,
the inferrred termination argument will be suggested.

## Equations

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

## Instances For

Specify a termination argument for well-founded termination:

```
termination_by a - b
```

indicates that termination of the currently defined recursive function follows
because the difference between the the arguments `a`

and `b`

.

If the fuction takes further argument after the colon, you can name them as follows:

```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```

If omitted, a termination argument will be inferred. If written as `termination_by?`

,
the inferrred termination argument will be suggested.

## Equations

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

## Instances For

Manually prove that the termination argument (as specified with `termination_by`

or inferred)
decreases at each recursive call.

By default, the tactic `decreasing_tactic`

is used.

## Equations

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

## Instances For

Termination hints are `termination_by`

and `decreasing_by`

, in that order.

## Equations

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

## Instances For

`letRecDecl`

matches the body of a let-rec declaration: a doc comment, attributes, and then
a let declaration without the `let`

keyword, such as `/-- foo -/ @[simp] bar := 1`

.

## Equations

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

## Instances For

`letRecDecls`

matches `letRecDecl,+`

, a comma-separated list of let-rec declarations (see `letRecDecl`

).

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

`unsafe t : α`

is an expression constructor which allows using unsafe declarations inside the
body of `t : α`

, by creating an auxiliary definition containing `t`

and using `implementedBy`

to
wrap it in a safe interface. It is required that `α`

is nonempty for this to be sound,
but even beyond that, an `unsafe`

block should be carefully inspected for memory safety because
the compiler is unable to guarantee the safety of the operation.

For example, the `evalExpr`

function is unsafe, because the compiler cannot guarantee that when
you call `evalExpr Foo ``Foo e`

that the type `Foo`

corresponds to the name `Foo`

, but in a
particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)`

is a correct usage.

## Equations

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

## Instances For

`binrel% r a b`

elaborates `r a b`

as a binary relation using the type propogation protocol in `Lean.Elab.Extra`

.

## Equations

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

## Instances For

`binrel_no_prop% r a b`

is similar to `binrel% r a b`

, but it coerces `Prop`

arguments into `Bool`

.

## Equations

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

## Instances For

`binop% f a b`

elaborates `f a b`

as a binary operation using the type propogation protocol in `Lean.Elab.Extra`

.

## Equations

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

## Instances For

`binop_lazy%`

is similar to `binop% f a b`

, but it wraps `b`

as a function from `Unit`

.

## Equations

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

## Instances For

`leftact% f a b`

elaborates `f a b`

as a left action using the type propogation protocol in `Lean.Elab.Extra`

.
In particular, it is like a unary operation with a fixed parameter `a`

, where only the right argument `b`

participates in the operator coercion elaborator.

## Equations

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

## Instances For

`rightact% f a b`

elaborates `f a b`

as a right action using the type propogation protocol in `Lean.Elab.Extra`

.
In particular, it is like a unary operation with a fixed parameter `b`

, where only the left argument `a`

participates in the operator coercion elaborator.

## Equations

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

## Instances For

`unop% f a`

elaborates `f a`

as a unary operation using the type propogation protocol in `Lean.Elab.Extra`

.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

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.

## Instances For

## Equations

- Lean.Parser.Term.completion = Lean.Parser.trailingNode `Lean.Parser.Term.completion 1024 0 (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun (x : Unit) => Lean.Parser.symbol ".")

## Instances For

## Equations

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

## Instances For

Syntax kind for syntax nodes representing the field of a projection in the `InfoTree`

.
Specifically, the `InfoTree`

node for a projection `s.f`

contains a child `InfoTree`

node
with syntax `(Syntax.node .none identProjKind #[`f])`

.

This is necessary because projection syntax cannot always be detected purely syntactically
(`s.f`

may refer to either the identifier `s.f`

or a projection `s.f`

depending on
the available context).

## Equations

- Lean.Parser.Term.identProjKind = `Lean.Parser.Term.identProj

## Instances For

## Equations

- Lean.Parser.Term.isIdent stx = (stx.isAntiquot || stx.isIdent)

## Instances For

`x.{u, ...}`

explicitly specifies the universes `u, ...`

of the constant `x`

.

## Equations

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

## Instances For

`x@e`

or `x:h@e`

matches the pattern `e`

and binds its value to the identifier `x`

.
If present, the identifier `h`

is bound to a proof of `x = e`

.

## Equations

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

## Instances For

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

## Instances For

## Equations

- Lean.Parser.Term.pipeCompletion = Lean.Parser.trailingNode `Lean.Parser.Term.pipeCompletion Lean.Parser.minPrec 0 (Lean.Parser.symbol " |>.")

## Instances For

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

## Equations

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

## Instances For

## Equations

- Lean.Parser.Term.bracketedBinderF = Lean.Parser.Term.bracketedBinder

## Instances For

## Equations

- Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_1 = { coe := fun (s : Lean.TSyntax `Lean.Parser.Term.bracketedBinderF) => { raw := s.raw } }

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

## Instances For

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

.

## Equations

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

## Instances For

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

## Instances For

## Instances For

## Equations

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

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

Implementation of the `show_term`

term elaborator.

## Equations

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

## Instances For

`match_expr`

support.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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