Getting started

Welcome

Run a program, check a proof, and find your way around leanlab.

-- Welcome to leanlab. This is a runnable Lean file.
-- Choose Run to check the proof and execute main.
-- First use downloads the Lean compiler (~46 MB), cached for later runs.
-- It runs as WebAssembly on your device. Your code is not uploaded.

def double (n : Nat) : Nat := n + n

-- A proof: double n is equal to n + n by definition.
-- rfl stands for reflexivity.
example (n : Nat) : double n = n + n := by
  rfl

def main : IO Unit := do
  IO.println "Welcome to leanlab."
  IO.println (double 21)

/-
Examples   Browse editable programs and proofs.
Playground Create, rename, and download your own files.
Learn      Follow lessons and check your exercises.
Syntax     Look up Lean keywords and mathematical symbols.

Open Guide for an explanation of this file.
Run locally explains how to use Lean on your computer.
Your files and lesson progress are saved on this device.
-/

Explanation

`def`

Defines a value or a function. double accepts a natural number and returns its sum with itself.

`example … := by rfl`

States an unnamed proposition and proves it by reflexivity: both sides reduce to the same expression.

`main : IO Unit`

The entry point of a program. IO.println writes a line to Output.

Expected output

Reference only. Run the file to check its actual result.

Welcome to leanlab.
42

Exercise

Change 21 to another natural number and run the file again. Then open Learn for guided exercises.