prev
up
next
import LeanFoundations.Logic
import LeanFoundations.PL

Preface #

Our work is heavily based on the Software Foundations (SF) series. Many of the examples and ideas are borrowed from SF. Check the license for more details.

We are inspired by the Software Foundations (SF) series. There should also be a systematic introduction to how to programming and verify algorithms in Lean. Yet, we are more ambitious in that we want to show how to make a (toy) lean out of lean itself and verify related code. We assume you know nothing about computer programming, but we do assume you are familiar with Unix-like operating systems (shell commands, text editors, file systems, etc) so that you know how to install lean, write the code and run other tools like lake or elan. If you are taking/teaching a course, then the first class should be about how to use a Unix-like operating system, system-wide software package management and install lean. And, some kind of proficiency of mathematics is helpful (and maybe necessary, e.g., you have to know natural numbers and mathematical induction on them).

The whole book is built on this Github repository. It is just an ordinary Lean package where the module comments are compiled as descriptions in this book, while the Lean code is displayed with a light green background. You can clone the repository, download the source code, or just make your own lake project and copy those lines.

Contents #

QuickStart #

Install Lean #

Command line #

First, install elan, the Lean version manager.

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

Then, install toolchains.

elan self update
elan default leanprover/lean4:stable

VSCode #

See here.

Homebrew #

brew install elan-init

Make a project #

lake new foo
cd foo
lake build
.lake/build/bin/foo

References #

See here.