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.
In order to run these samples you need a working Lean 4 environment. See Quickstart instructions on how to set that up.
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.
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.
Every language needs a simple hello world sample.
Explore more standard input processing with a simple guess-my-number game.
CSV parser is the simplest practical CSV parser you can write in Lean.
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.
Explore how you can extend the Lean syntax to implement the popular python-style List Comprehension.