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
orprotected
noncomputable
unsafe
partial
ornonrec
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
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 righthand side of a declaration, one of:
:= expr
(a "simple declaration") a sequence of
 pat => expr
(a declaration by equations), shorthand for amatch
where
and then a sequence offield := 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
, 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 namespaceNat
is given the full nameNat.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 oropen
.  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 alreadydeclared 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. The
variable
command is also able to add typeclass parameters. 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, or instance implicit (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.
See Variables and Sections from Theorem Proving in Lean for a more detailed discussion.
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
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 typeuniverse parameter. /
def id₁.{u} (α : Type u) (a : α) := a
/ Implicit typeuniverse 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 righthand 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
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 userdefined extensions. The setting is active until the end of the current section
or namespace
or the end of the file.
Autocompletion 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
, likeopen
, and  visible from outside the current namespace
N
asN.name₁
andN.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 nonprotected names inSome.Namespace.Path1
andSome.Namespace.Path2
available without the prefix, so thatSome.Namespace.Path1.x
andSome.Namespace.Path2.y
can be referred to by writing onlyx
andy
. 
open Some.Namespace.Path hiding def1 def2
opens all nonprotected names inSome.Namespace.Path
exceptdef1
anddef2
. 
open Some.Namespace.Path (def1 def2)
only makesSome.Namespace.Path.def1
andSome.Namespace.Path.def2
available without the full prefix, soSome.Namespace.Path.def3
would be unaffected.This works even if
def1
anddef2
areprotected
. 
open Some.Namespace.Path renaming def1 → def1', def2 → def2'
same asopen Some.Namespace.Path (def1 def2)
butdef1
/def2
's names are changed todef1'
/def2'
.This works even if
def1
anddef2
areprotected
. 
open scoped Some.Namespace.Path1 Some.Namespace.Path2
only opens [scoped instances], notations, and attributes fromNamespace1
andNamespace2
; it does not make any other name available. 
open <any of the open shapes above> in
makes the namesopen
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 autogenerated 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
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
Noop parser used as syntax kind for attaching remaining whitespace to 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
orprotected
noncomputable
unsafe
partial
ornonrec
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
orprotected
noncomputable
unsafe
partial
ornonrec
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.