Syntax quotation for terms.

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

Syntax quotation for (sequences of) commands.
The identical syntax for term quotations takes priority,
so ambiguous quotations like ``($x $y)`

will be parsed as an application,
not two commands. Use ``($x:command $y:command)`

instead.
Multiple commands will be put in a ``null`

node,
but a single command will not (so that you can directly
match against a quotation in a command kind's elaborator).

## Equations

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

## Instances For

`/-! <text> -/`

defines a *module docstring* that can be displayed by documentation generation
tools. The string is associated with the corresponding position in the file. It can be used
multiple times in the same file.

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

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

`declModifiers`

is the collection of modifiers on a declaration:

- a doc comment
`/-- ... -/`

- a list of attributes
`@[attr1, attr2]`

- a visibility specifier,
`private`

or`protected`

`noncomputable`

`unsafe`

`partial`

or`nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers`

is the same as `declModifiers`

, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec`

/ `where`

definitions.

## Equations

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

## Instances For

`declId`

matches `foo`

or `foo.{u,v}`

: an identifier possibly followed by a list of universe names

## Equations

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

## Instances For

`declSig`

matches the signature of a declaration with required type: a list of binders and then `: type`

## Equations

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

## Instances For

`optDeclSig`

matches the signature of a declaration with optional type: a list of binders and then possibly `: type`

## Equations

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

## Instances For

Right-hand side of a `:=`

in a declaration, a term.

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

`declVal`

matches the right-hand side of a declaration, one of:

`:= expr`

(a "simple declaration")- a sequence of
`| pat => expr`

(a declaration by equations), shorthand for a`match`

`where`

and then a sequence of`field := value`

initializers, shorthand for a structure constructor

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

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

In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List α`

is the list of elements of type `α`

, and is defined as follows:

```
inductive List (α : Type u) where
| nil
| cons (head : α) (tail : List α)
```

A list of elements of type `α`

is either the empty list, `nil`

,
or an element `head : α`

followed by a list `tail : List α`

.
For more information about inductive types.

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

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

/`end`

pair delimits the scope of `variable`

, `include, `

open`, `

set_option`, and `

local`commands. Sections can be nested.`

section <id>`provides a label to the section that has to appear with the matching`

end`. In either case, the `

end` can be omitted, in which case the section is
closed at the end of the file.

## Equations

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

## Instances For

`namespace <id>`

opens a section with label `<id>`

that influences naming and name resolution inside
the section:

- Declarations names are prefixed:
`def seventeen : ℕ := 17`

inside a namespace`Nat`

is given the full name`Nat.seventeen`

. - Names introduced by
`export`

declarations are also prefixed by the identifier. - All names starting with
`<id>.`

become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or`open`

. - Within a namespace, declarations can be
`protected`

, which excludes them from the effects of opening the namespace.

As with `section`

, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>`

or the end of the file.

`namespace`

also acts like `section`

in delimiting the scope of `variable`

, `open`

, and other scoped commands.

## Equations

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

## Instances For

Declares one or more typed variables, or modifies whether already-declared variables are implicit.

Introduces variables that can be used in definitions within the same `namespace`

or `section`

block.
When a definition mentions a variable, Lean will add it as an argument of the definition. This is
useful in particular when writing many definitions that have parameters in common (see below for an
example).

Variable declarations have the same flexibility as regular function paramaters. In particular they
can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
can be anonymous). This can be changed, for instance one can turn explicit variable `x`

into an
implicit one with `variable {x}`

. Note that currently, you should avoid changing how variables are
bound and declare new variables at the same time; see [issue 2789] for more on this topic.

In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that
changes to the proof cannot change the statement of the overall theorem. Instead, variables are only
available to the proof if they have been mentioned in the theorem header or in an `include`

command
or are instance implicit and depend only on such variables.

See *Variables and Sections* from Theorem Proving in Lean for a more detailed
discussion.

(Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github)

## Examples #

```
section
variable
{α : Type u} -- implicit
(a : α) -- explicit
[instBEq : BEq α] -- instance implicit, named
[Hashable α] -- instance implicit, anonymous
def isEqual (b : α) : Bool :=
a == b
#check isEqual
-- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool
variable
{a} -- `a` is implicit now
def eqComm {b : α} := a == b ↔ b == a
#check eqComm
-- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop
end
```

The following shows a typical use of `variable`

to factor out definition arguments:

```
variable (Src : Type)
structure Logger where
trace : List (Src × String)
#check Logger
-- Logger (Src : Type) : Type
namespace Logger
-- switch `Src : Type` to be implicit until the `end Logger`
variable {Src}
def empty : Logger Src where
trace := []
#check empty
-- Logger.empty {Src : Type} : Logger Src
variable (log : Logger Src)
def len :=
log.trace.length
#check len
-- Logger.len {Src : Type} (log : Logger Src) : Nat
variable (src : Src) [BEq Src]
-- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments
def filterSrc :=
log.trace.filterMap
fun (src', str') => if src' == src then some str' else none
#check filterSrc
-- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String
def lenSrc :=
log.filterSrc src |>.length
#check lenSrc
-- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat
end Logger
```

The following example demonstrates availability of variables in proofs:

```
variable
{α : Type} -- available in the proof as indirectly mentioned through `a`
[ToString α] -- available in the proof as `α` is included
(a : α) -- available in the proof as mentioned in the header
{β : Type} -- not available in the proof
[ToString β] -- not available in the proof
theorem ex : a = a := rfl
```

After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis:

```
included section variable '[ToString α]' is not used in 'ex', consider excluding it
```

In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.

## Equations

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

## Instances For

Declares one or more universe variables.

`universe u v`

`Prop`

, `Type`

, `Type u`

and `Sort u`

are types that classify other types, also known as
*universes*. In `Type u`

and `Sort u`

, the variable `u`

stands for the universe's *level*, and a
universe at level `u`

can only classify universes that are at levels lower than `u`

. For more
details on type universes, please refer to the relevant chapter of Theorem Proving in Lean.

Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe`

keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.

```
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a
/- Implicit type-universe parameter, equivalent to `id₁`.
Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a
/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```

On a more technical note, using a universe variable only in the right-hand side of a definition causes an error if the universe has not been declared previously.

```
def L₁.{u} := List (Type u)
-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
universe u
def L₃ := List (Type u)
```

## Examples #

```
universe u v w
structure Pair (α : Type u) (β : Type v) : Type (max u v) where
a : α
b : β
#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```

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

Displays all available tactic tags, with documentation.

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

`set_option <id> <value>`

sets the option `<id>`

to `<value>`

. Depending on the type of the option,
the value can be `true`

, `false`

, a string, or a numeral. Options are used to configure behavior of
Lean as well as user-defined extensions. The setting is active until the end of the current `section`

or `namespace`

or the end of the file.
Auto-completion is available for `<id>`

to list available options.

`set_option <id> <value> in <command>`

sets the option for just a single command:

```
set_option pp.all true in
#check 1 + 1
```

Similarly, `set_option <id> <value> in`

can also be used inside terms and tactics to set an option
only in a single term or tactic.

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

Adds names from other namespaces to the current namespace.

The command `export Some.Namespace (name₁ name₂)`

makes `name₁`

and `name₂`

:

- visible in the current namespace without prefix
`Some.Namespace`

, like`open`

, and - visible from outside the current namespace
`N`

as`N.name₁`

and`N.name₂`

.

## Examples #

```
namespace Morning.Sky
def star := "venus"
end Morning.Sky
namespace Evening.Sky
export Morning.Sky (star)
-- `star` is now in scope
#check star
end Evening.Sky
-- `star` is visible in `Evening.Sky`
#check Evening.Sky.star
```

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

Makes names from other namespaces visible without writing the namespace prefix.

Names that are made available with `open`

are visible within the current `section`

or `namespace`

block. This makes referring to (type) definitions and theorems easier, but note that it can also
make [scoped instances], notations, and attributes from a different namespace available.

The `open`

command can be used in a few different ways:

`open Some.Namespace.Path1 Some.Namespace.Path2`

makes all non-protected names in`Some.Namespace.Path1`

and`Some.Namespace.Path2`

available without the prefix, so that`Some.Namespace.Path1.x`

and`Some.Namespace.Path2.y`

can be referred to by writing only`x`

and`y`

.`open Some.Namespace.Path hiding def1 def2`

opens all non-protected names in`Some.Namespace.Path`

except`def1`

and`def2`

.`open Some.Namespace.Path (def1 def2)`

only makes`Some.Namespace.Path.def1`

and`Some.Namespace.Path.def2`

available without the full prefix, so`Some.Namespace.Path.def3`

would be unaffected.This works even if

`def1`

and`def2`

are`protected`

.`open Some.Namespace.Path renaming def1 → def1', def2 → def2'`

same as`open Some.Namespace.Path (def1 def2)`

but`def1`

/`def2`

's names are changed to`def1'`

/`def2'`

.This works even if

`def1`

and`def2`

are`protected`

.`open scoped Some.Namespace.Path1 Some.Namespace.Path2`

**only**opens [scoped instances], notations, and attributes from`Namespace1`

and`Namespace2`

; it does**not**make any other name available.`open <any of the open shapes above> in`

makes the names`open`

-ed visible only in the next command or expression.

## Examples #

```
/-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
namespace Combinator.Calculus
def I (a : α) : α := a
def K (a : α) : β → α := fun _ => a
def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
end Combinator.Calculus
section
-- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
-- until the section ends
open Combinator.Calculus
theorem SKx_eq_K : S K x = I := rfl
end
-- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
open Combinator.Calculus in
theorem SKx_eq_K' : S K x = I := rfl
section
-- open only `S` and `K` under `Combinator.Calculus`
open Combinator.Calculus (S K)
theorem SKxy_eq_y : S K x y = y := rfl
-- `I` is not in scope, we have to use its full path
theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
end
section
open Combinator.Calculus
renaming
I → identity,
K → konstant
#check identity
#check konstant
end
section
open Combinator.Calculus
hiding S
#check I
#check K
end
section
namespace Demo
inductive MyType
| val
namespace N1
scoped infix:68 " ≋ " => BEq.beq
scoped instance : BEq MyType where
beq _ _ := true
def Alias := MyType
end N1
end Demo
-- bring `≋` and the instance in scope, but not `Alias`
open scoped Demo.N1
#check Demo.MyType.val == Demo.MyType.val
#check Demo.MyType.val ≋ Demo.MyType.val
-- #check Alias -- unknown identifier 'Alias'
end
```

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

Adds a docstring to an existing declaration, replacing any existing docstring.
The provided docstring should be written as a docstring for the `add_decl_doc`

command, as in

```
/-- My new docstring -/
add_decl_doc oldDeclaration
```

This is useful for auto-generated declarations for which there is no place to write a docstring in the source code.

Parent projections in structures are an example of this:

```
structure Triple (α β γ : Type) extends Prod α β where
thrd : γ
/-- Extracts the first two projections of a triple. -/
add_decl_doc Triple.toProd
```

Documentation can only be added to declarations in the same module.

## Equations

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

## Instances For

Register a tactic tag, saving its user-facing name and docstring.

Tactic tags can be used by documentation generation tools to classify related tactics.

## Equations

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

## Instances For

Add more documentation as an extension of the documentation for a given tactic.

The extended documentation is placed in the command's docstring. It is shown as part of a bulleted list, so it should be brief.

## Equations

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

## Instances For

This is an auxiliary command for generation constructor injectivity theorems for
inductive types defined at `Prelude.lean`

.
It is meant for bootstrapping purposes only.

## Equations

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

## Instances For

`include eeny meeny`

instructs Lean to include the section `variable`

s `eeny`

and `meeny`

in all
theorems in the remainder of the current section, differing from the default behavior of
conditionally including variables based on use in the theorem header. Other commands are
not affected. `include`

is usually followed by `in theorem ...`

to limit the inclusion
to the subsequent declaration.

## Equations

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

## Instances For

`omit`

instructs Lean to not include a variable previously `include`

d. Apart from variable names, it
can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`

, in
which case all instance variables that unify with the given type are omitted. `omit`

should usually
only be used in conjunction with `in`

in order to keep the section structure simple.

## Equations

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

## Instances For

No-op parser used as syntax kind for attaching remaining whitespace at the end of the input.

## Equations

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

## Instances For

`declModifiers`

is the collection of modifiers on a declaration:

- a doc comment
`/-- ... -/`

- a list of attributes
`@[attr1, attr2]`

- a visibility specifier,
`private`

or`protected`

`noncomputable`

`unsafe`

`partial`

or`nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers`

is the same as `declModifiers`

, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec`

/ `where`

definitions.

## Instances For

`declModifiers`

is the collection of modifiers on a declaration:

- a doc comment
`/-- ... -/`

- a list of attributes
`@[attr1, attr2]`

- a visibility specifier,
`private`

or`protected`

`noncomputable`

`unsafe`

`partial`

or`nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers`

is the same as `declModifiers`

, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec`

/ `where`

definitions.

## Instances For

`set_option opt val in e`

is like `set_option opt val`

but scoped to a single term.
It sets the option `opt`

to the value `val`

in the term `e`

.

## Equations

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

## Instances For

`set_option opt val in tacs`

(the tactic) acts like `set_option opt val`

at the command level,
but it sets the option only within the tactics `tacs`

.

## Equations

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