6.1. Messages🔗

Lean produces three kinds of messages:

Errors

Errors are produced when an inconsistency in the code means that it can't be processed. Examples include syntax errors (e.g. a missing )) and type errors such as attempting to add a natural number to a function.

Warnings

Warnings describe potential problems with the code, such as the presence of sorry. Unlike with errors, the code is not meaningless; however, warnings deserve careful attention.

Information

Information doesn't indicate any problem with the code, and includes output from commands such as #check and #eval.

Lean can check that a command produces the expected messages. If the messages match, then any errors are disregarded; this can be used to ensure that the right errors occur. If they don't, an error is produced. You can use the #guard_msgs command to indicate which messages are expected.

Here is an example:

Including a message category in parentheses after #guard_msgs causes it to check only the specified category, letting others through. In this example, #eval issues an error due to the presence of sorry, but the warning that is always issued for sorry is displayed as usual:

declaration uses 'sorry'

Without the configuration, both messages are captured:

❌️ Docstring on `#guard_msgs` does not match generated message:

warning: declaration uses 'sorry'
---
error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.

To attempt to evaluate anyway despite the risks, use the '#eval!' command.

Some examples in this book use #guard_msgs to indicate expected errors.

6.2. Importing Files🔗

The goal of Lean's front end is to interpret user input, construct formal expressions, and check that they are well-formed and type-correct. Lean also supports the use of various editors, which provide continuous checking and feedback. More information can be found on the Lean documentation pages.

The definitions and theorems in Lean's standard library are spread across multiple files. Users may also wish to make use of additional libraries, or develop their own projects across multiple files. When Lean starts, it automatically imports the contents of the library Init folder, which includes a number of fundamental definitions and constructions. As a result, most of the examples we present here work “out of the box.”

If you want to use additional files, however, they need to be imported manually, via an import statement at the beginning of a file. The command

import Bar.Baz.Blah

imports the file Bar/Baz/Blah.olean, where the descriptions are interpreted relative to the Lean search path. Information as to how the search path is determined can be found on the documentation pages. By default, it includes the standard library directory, and (in some contexts) the root of the user's local project.

Importing is transitive. In other words, if you import Foo and Foo imports Bar, then you also have access to the contents of Bar, and do not need to import it explicitly.

6.3. More on Sections🔗

Lean provides various sectioning mechanisms to help structure a theory. You saw in Variables and Sections that the section command makes it possible not only to group together elements of a theory that go together, but also to declare variables that are inserted as arguments to theorems and definitions, as necessary. Remember that the point of the variable command is to declare variables for use in theorems, as in the following example:

double y : Nat

double (2 * x) : Nat

t1 y : ∀ (y_1 : Nat), double (y + y_1) = double y + double y_1

t1 (2 * x) : ∀ (y : Nat), double (2 * x + y) = double (2 * x) + double y

The definition of double does not have to declare x as an argument; Lean detects the dependence and inserts it automatically. Similarly, Lean detects the occurrence of x in t1 and t2, and inserts it automatically there, too. Note that double does not have y as argument. Variables are only included in declarations where they are actually used.

6.4. More on Namespaces🔗

In Lean, identifiers are given by hierarchical names like Foo.Bar.baz. We saw in Namespaces that Lean provides mechanisms for working with hierarchical names. The command namespace Foo causes Foo to be prepended to the name of each definition and theorem until end Foo is encountered. The command open Foo then creates temporary aliases to definitions and theorems that begin with prefix Foo.

Foo.bar : Nat

Foo.bar : Nat

The following definition

is treated as a macro, and expands to

Although the names of theorems and definitions have to be unique, the aliases that identify them do not. When we open a namespace, an identifier may be ambiguous. Lean tries to use type information to disambiguate the meaning in context, but you can always disambiguate by giving the full name. To that end, the string _root_ is an explicit description of the empty prefix.

String.add (a b : String) : String

Bool.add (a b : Bool) : Bool

add (α β : Type) : Type

"hello".add "world" : String

true.add false : Bool

_root_.add Nat Nat : Type

We can prevent the shorter alias from being created by using the protected keyword:

Foo.bar : Nat

This is often used for names like Nat.rec and Nat.recOn, to prevent overloading of common names.

The open command admits variations. The command

Nat.zero : Nat

3

creates aliases for only the identifiers listed. The command

Nat.zero : Nat

3

creates aliases for everything in the Nat namespace except the identifiers listed.

7

creates aliases renaming Nat.mul to times and Nat.add to plus.

It is sometimes useful to export aliases from one namespace to another, or to the top level. The command

creates aliases for succ, add, and sub in the current namespace, so that whenever the namespace is open, these aliases are available. If this command is used outside a namespace, the aliases are exported to the top level.

6.5. Attributes🔗

The main function of Lean is to translate user input to formal expressions that are checked by the kernel for correctness and then stored in the environment for later use. But some commands have other effects on the environment, either assigning attributes to objects in the environment, defining notation, or declaring instances of type classes, as described in the chapter on type classes. Most of these commands have global effects, which is to say, they remain in effect not only in the current file, but also in any file that imports it. However, such commands often support the local modifier, which indicates that they only have effect until the current section or namespace is closed, or until the end of the current file.

In Using the Simplifier, we saw that theorems can be annotated with the [simp] attribute, which makes them available for use by the simplifier. The following example defines the prefix relation on lists, proves that this relation is reflexive, and assigns the [simp] attribute to that theorem.

The simplifier then proves isPrefix [1, 2, 3] [1, 2, 3] by rewriting it to True.

One can also assign the attribute any time after the definition takes place:

In all these cases, the attribute remains in effect in any file that imports the one in which the declaration occurs. Adding the local modifier restricts the scope:

For another example, we can use the instance command to assign the notation ≤ to the isPrefix relation. That command, which will be explained in the chapter on type classes, works by assigning an [instance] attribute to the associated definition.

That assignment can also be made local:

In Notation below, we will discuss Lean's mechanisms for defining notation, and see that they also support the local modifier. However, in Setting Options, we will discuss Lean's mechanisms for setting options, which does not follow this pattern: options can only be set locally, which is to say, their scope is always restricted to the current section or current file.

6.6. More on Implicit Arguments🔗

In Implicit Arguments, we saw that if Lean displays the type of a term t as {x : α} → β x, then the curly brackets indicate that x has been marked as an implicit argument to t. This means that whenever you write t, a placeholder, or “hole,” is inserted, so that t is replaced by @t _. If you don't want that to happen, you have to write @t instead.

Notice that implicit arguments are inserted eagerly. Suppose we define a function f : (x : Nat) → {y : Nat} → (z : Nat) → Nat. Then, when we write the expression f 7 without further arguments, it is parsed as @f 7 _.

Lean offers a weaker annotation which specifies that a placeholder should only be added before a subsequent explicit argument. It can be written with double braces, so the type of f would be f : (x : Nat) → {{y : Nat}} → (z : Nat) → Nat. With this annotation, the expression f 7 would be parsed as is, whereas f 7 3 would be parsed as @f 7 _ 3, just as it would be with the strong annotation. This annotation can also be written as ⦃y : Nat⦄, where the Unicode brackets are entered as \{{ and \}}, respectively.

To illustrate the difference, consider the following example, which shows that a reflexive euclidean relation is both symmetric and transitive.

euclr : r ?m.460 ?m.461 → r ?m.460 ?m.462 → r ?m.461 ?m.462

The results are broken down into small steps: th1 shows that a relation that is reflexive and euclidean is symmetric, and th2 shows that a relation that is symmetric and euclidean is transitive. Then th3 combines the two results. But notice that we have to manually disable the implicit arguments in euclr, because otherwise too many implicit arguments are inserted. The problem goes away if we use weak implicit arguments:

euclr : Euclidean r

There is a third kind of implicit argument that is denoted with square brackets, [ and ]. These are used for type classes, as explained in the chapter on type classes.

6.7. Notation🔗

Identifiers in Lean can include any alphanumeric characters, including Greek characters (other than ∀ , Σ , and λ , which, as we have seen, have a special meaning in the dependent type theory). They can also include subscripts, which can be entered by typing \_ followed by the desired subscripted character.

Lean's parser is extensible, which is to say, we can define new notation.

Lean's syntax can be extended and customized by users at every level, ranging from basic “mixfix” notations to custom elaborators. In fact, all builtin syntax is parsed and processed using the same mechanisms and APIs open to users. In this section, we will describe and explain the various extension points.

While introducing new notations is a relatively rare feature in programming languages and sometimes even frowned upon because of its potential to obscure code, it is an invaluable tool in formalization for expressing established conventions and notations of the respective field succinctly in code. Going beyond basic notations, Lean's ability to factor out common boilerplate code into (well-behaved) macros and to embed entire custom domain specific languages (DSLs) to textually encode subproblems efficiently and readably can be of great benefit to both programmers and proof engineers alike.

0

6.8. Coercions🔗

In Lean, the type of natural numbers, Nat, is different from the type of integers, Int. But there is a function Int.ofNat that embeds the natural numbers in the integers, meaning that we can view any natural number as an integer, when needed. Lean has mechanisms to detect and insert coercions of this sort. Coercions can be explicitly requested using the overloaded ↑ operator.

i + ↑m : Int

i + ↑m + j : Int

i + ↑m + ↑n : Int

6.9. Displaying Information🔗

There are a number of ways in which you can query Lean for information about its current state and the objects and theorems that are available in the current context. You have already seen two of the most common ones, #check and #eval. Remember that #check is often used in conjunction with the @ operator, which makes all of the arguments to a theorem or definition explicit. In addition, you can use the #print command to get information about any identifier. If the identifier denotes a definition or theorem, Lean prints the type of the symbol, and its definition. If it is a constant or an axiom, Lean indicates that fact, and shows the type.

Eq.{u_1} {α : Sort u_1} : α → α → Prop

@Eq : {α : Sort u_1} → α → α → Prop

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

@Eq.symm : ∀ {α : Sort u_1} {a b : α}, a = b → b = a

theorem Eq.symm.{u} : ∀ {α : Sort u} {a b : α}, a = b → b = a :=
fun {α} {a b} h => h ▸ rfl

And (a b : Prop) : Prop

And.intro {a b : Prop} (left : a) (right : b) : a ∧ b

@And.intro : ∀ {a b : Prop}, a → b → a ∧ b

foo.{u} {α : Type u} (x : α) : α

@foo : {α : Type u_1} → α → α

def foo.{u} : {α : Type u} → α → α :=
fun {α} x => x

6.10. Setting Options🔗

Lean maintains a number of internal variables that can be set by users to control its behavior. The syntax for doing so is as follows:

set_option <name> <value>

One very useful family of options controls the way Lean's pretty printer displays terms. The following options take an input of true or false:

pp.explicit  : display implicit arguments
pp.universes : display hidden universe parameters
pp.notation  : display output using defined notations

As an example, the following settings yield much longer output:

@Eq.{1} Nat
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
    (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  (@OfNat.ofNat.{0} Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) : Prop

@Eq.{1} (Nat → Nat)
  (fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 2) (instOfNatNat (nat_lit 2))))
  fun x =>
  @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
    (@OfNat.ofNat.{0} Nat (nat_lit 3) (instOfNatNat (nat_lit 3)))

(fun x =>
    @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x
      (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
  (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))) : Nat

The command set_option pp.all true carries out these settings all at once, whereas set_option pp.all false reverts to the previous values. Pretty printing additional information is often very useful when you are debugging a proof, or trying to understand a cryptic error message. Too much information can be overwhelming, though, and Lean's defaults are generally sufficient for ordinary interactions.

6.11. Using the Library🔗

To use Lean effectively you will inevitably need to make use of definitions and theorems in the library. Recall that the import command at the beginning of a file imports previously compiled results from other files, and that importing is transitive; if you import Foo and Foo imports Bar, then the definitions and theorems from Bar are available to you as well. But the act of opening a namespace, which provides shorter names, does not carry over. In each file, you need to open the namespaces you wish to use.

In general, it is important for you to be familiar with the library and its contents, so you know what theorems, definitions, notations, and resources are available to you. Below we will see that Lean's editor modes can also help you find things you need, but studying the contents of the library directly is often unavoidable. Lean's standard library can be found online, on GitHub:

• https://github.com/leanprover/lean4/tree/master/src/Init

• https://github.com/leanprover/lean4/tree/master/src/Std

You can see the contents of these directories and files using GitHub's browser interface. If you have installed Lean on your own computer, you can find the library in the lean folder, and explore it with your file manager. Comment headers at the top of each file provide additional information.

Lean's library developers follow general naming guidelines to make it easier to guess the name of a theorem you need, or to find it using tab completion in editors with a Lean mode that supports this, which is discussed in the next section. Identifiers are generally camelCase, and types are CamelCase. For theorem names, we rely on descriptive names where the different components are separated by _s. Often the name of theorem simply describes the conclusion:

Nat.succ_ne_zero (n : Nat) : n.succ ≠ 0

Nat.zero_add (n : Nat) : 0 + n = n

Nat.mul_one (n : Nat) : n * 1 = n

Nat.le_of_succ_le_succ {n m : Nat} : n.succ ≤ m.succ → n ≤ m

Remember that identifiers in Lean can be organized into hierarchical namespaces. For example, the theorem named le_of_succ_le_succ in the namespace Nat has full name Nat.le_of_succ_le_succ, but the shorter name is made available by the command open Nat (for names not marked as protected). We will see in the chapters on inductive types and structures and records that defining structures and inductive data types in Lean generates associated operations, and these are stored in a namespace with the same name as the type under definition. For example, the product type comes with the following operations:

@Prod.mk : {α : Type u_1} → {β : Type u_2} → α → β → α × β

@Prod.fst : {α : Type u_1} → {β : Type u_2} → α × β → α

@Prod.snd : {α : Type u_1} → {β : Type u_2} → α × β → β

@Prod.rec : {α : Type u_2} →
  {β : Type u_3} → {motive : α × β → Sort u_1} → ((fst : α) → (snd : β) → motive (fst, snd)) → (t : α × β) → motive t

The first is used to construct a pair, whereas the next two, Prod.fst and Prod.snd, project the two elements. The last, Prod.rec, provides another mechanism for defining functions on a product in terms of a function on the two components. Names like Prod.rec are protected, which means that one has to use the full name even when the Prod namespace is open.

With the propositions as types correspondence, logical connectives are also instances of inductive types, and so we tend to use dot notation for them as well:

@And.intro : ∀ {a b : Prop}, a → b → a ∧ b

@And.casesOn : {a b : Prop} →
  {motive : a ∧ b → Sort u_1} → (t : a ∧ b) → ((left : a) → (right : b) → motive ⋯) → motive t

@And.left : ∀ {a b : Prop}, a ∧ b → a

@And.right : ∀ {a b : Prop}, a ∧ b → b

@Or.inl : ∀ {a b : Prop}, a → a ∨ b

@Or.inr : ∀ {a b : Prop}, b → a ∨ b

@Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c

@Exists.intro : ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → Exists p

@Exists.elim : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b

@Eq.refl : ∀ {α : Sort u_1} (a : α), a = a

@Eq.subst : ∀ {α : Sort u_1} {motive : α → Prop} {a b : α}, a = b → motive a → motive b

6.12. Auto Bound Implicit Arguments🔗

In the previous section, we have shown how implicit arguments make functions more convenient to use. However, functions such as compose are still quite verbose to define. Note that the universe polymorphic compose is even more verbose than the one previously defined.

You can avoid the universe command by providing the universe parameters when defining compose.

Lean 4 supports a new feature called auto bound implicit arguments. It makes functions such as compose much more convenient to write. When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument. With this feature we can write compose as

@compose : {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ

Note that Lean inferred a more general type using Sort instead of Type.

Although we love this feature and use it extensively when implementing Lean, we realize some users may feel uncomfortable with it. Thus, you can disable it using the command set_option autoImplicit false.

6.13. Implicit Lambdas🔗

When the expected type of an expression is a function that is awaiting implicit arguments, the elaborator automatically introduces the corresponding lambdas. For example, pure's type states that the first argument is an implicit type α, but ReaderT.pure's first agument is the reader monad's context type ρ. It is automatically surrounded with a fun {α} => ..., which allows the elaborator to correctly fill in the implicit arguments in the body.

Users can disable the implicit lambda feature by using @ or writing a lambda expression with {} or [] binder annotations. Here are few examples

6.14. Sugar for Simple Functions🔗

Lean includes a notation for describing simple functions using anonymous placeholders rather than fun. When · occurs as part of a term, the nearest enclosing parentheses become a function with the · as its argument. If the parentheses include multiple placeholders without other intervening parentheses, then they are made into arguments from left to right. Here are a few examples:

fun x => x + 1 : Nat → Nat

fun x => 2 - x : Nat → Nat

120

fun x1 x2 => f x1 1 x2 : Nat → Nat → Nat

[1, 3, 5]

Nested parentheses introduce new functions. In the following example, two different lambda expressions are created:

fun x => (x, fun x => x + 1) : ?m.2 → ?m.2 × (Nat → Nat)

6.15. Named Arguments🔗

Named arguments enable you to specify an argument for a parameter by matching the argument with its name rather than with its position in the parameter list. If you don't remember the order of the parameters but know their names, you can send the arguments in any order. You may also provide the value for an implicit parameter when Lean failed to infer it. Named arguments also improve the readability of your code by identifying what each argument represents.

10

In the following examples, we illustrate the interaction between named and default arguments.

You can use .. to provide missing explicit arguments as _. This feature combined with named arguments is useful for writing patterns. Here is an example:

Ellipses are also useful when explicit arguments can be automatically inferred by Lean, and we want to avoid a sequence of _s.