Deprecated lean4-samples repository.

This repository was prepared during the early development of Lean, and is now deprecated and unmaintained.

We do not recommend using it as a source for examples or teaching materials. Please see

• the Lean language documentation and
• the Lean community webpage

for getting started.

The future of this repo

If someone has a clear plan for this repository, and would like to take over maintainership and develop it into an up-to-date resource, please contact us on zulip.

Old README contents

Code samples for Lean 4. These samples are designed to work inside Visual Studio Code with the Lean4 "extension". The extension will install the Lean4 compiler and language service for you so it is easy to setup - see the Quick Start for more information.

Currently each folder must be opened separately in Visual Studio Code for that sample to compile correctly since each folder contains a separate Lean Package that is buildable using lake build. Lake is the build system that comes with Lean.

Get started

In order to run these samples you need a working Lean 4 environment. See Quickstart instructions on how to set that up.

Use Gitpod

You can also use Gitpod to browse these samples and it will setup a working Lean 4 environment for you. Start by pointing your browser at https://gitpod.io/#https://github.com/leanprover/lean4-samples then when lean is installed use File/Open Folder... to open the sample that you want to play with.

See Demo Video showing how to do this.

Use Github Codespaces

If you have a Github Team or Enterprise account you can also play with these samples in a Github Codespace.

See Demo Video showing how it works.

Hello world

Every language needs a simple hello world sample.

Guess My Number

Explore more standard input processing with a simple guess-my-number game.

CSV Parser

CSV parser is the simplest practical CSV parser you can write in Lean.

Rubik's cube

Rubik's cube is an example showing how to build custom user widgets for the InfoView using TypeScript and Lake. Given a sequence of moves, it renders a Rubik's cube in 3D which can be animated with the movement of a slider.

List Comprehension using Syntax Extension

Explore how you can extend the Lean syntax to implement the popular python-style List Comprehension.