Getting Lean

Before writing and running programs written in Lean, you'll need to set up Lean on your own computer. The Lean tooling consists of the following:

• elan manages the Lean compiler toolchains, similarly to rustup or ghcup.

• lake builds Lean packages and their dependencies, similarly to cargo, make, or Gradle.

• lean type checks and compiles individual Lean files as well as providing information to programmer tools about files that are currently being written. Normally, lean is invoked by other tools rather than directly by users.

• Plugins for editors, such as Visual Studio Code or Emacs, that communicate with lean and present its information conveniently.

Please refer to the Lean manual for up-to-date instructions for installing Lean.

Typographical Conventions

Code examples that are provided to Lean as input are formatted like this:

The last line above (beginning with #eval) is a command that instructs Lean to calculate an answer. Lean's replies are formatted like this:

8

Error messages returned by Lean are formatted like this:

application type mismatch
  add1 "seven"
argument
  "seven"
has type
  String : Type
but is expected to have type
  Nat : Type

Warnings are formatted like this:

declaration uses 'sorry'

Unicode

Idiomatic Lean code makes use of a variety of Unicode characters that are not part of ASCII. For instance, Greek letters like α and β and the arrow → both occur in the first chapter of this book. This allows Lean code to more closely resemble ordinary mathematical notation.

With the default Lean settings, both Visual Studio Code and Emacs allow these characters to be typed with a backslash (\) followed by a name. For example, to enter α, type \alpha. To find out how to type a character in Visual Studio Code, point the mouse at it and look at the tooltip. In Emacs, use C-c C-k with point on the character in question.

Release history

About the Author

David Thrane Christiansen has been using functional languages for twenty years, and dependent types for ten. Together with Daniel P. Friedman, he wrote The Little Typer, an introduction to the key ideas of dependent type theory. He has a Ph.D. from the IT University of Copenhagen. During his studies, he was a major contributor to the first version of the Idris language. Since leaving academia, he has worked as a software developer at Galois in Portland, Oregon and Deon Digital in Copenhagen, Denmark, and he was the Executive Director of the Haskell Foundation. At the time of writing, he is employed at the Lean Focused Research Organization working full-time on Lean.

License

The original version of the book was written by David Thrane Christiansen on contract to Microsoft Corporation, who generously released it under a Creative Commons Attribution 4.0 International License. The current version has been modified by the author from the original version to account for changes in newer versions of Lean. A detailed account of the changes can be found in the book's source code repository.