# Documentation

## Lean.Elab.BuiltinCommand

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Elab.Command.withNamespace {α : Type} (ns : Lake.Name) (elabFn : ) :
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
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
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

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

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. 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
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
@[implemented_by Lean.Elab.Command.elabEvalUnsafe]
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
Instances For
Equations
Instances For
Equations
Instances For