Module 1: Lean as a programming language

The playground runs the latest Lean in your browser. Locally, the file is Exercises/Programming.lean and you check it with lake exe check Programming.

Guide

Read: Functional Programming in Lean, chapter 1 ("Getting to Know Lean").

Key ideas:

#eval evaluates an expression and #check shows its type.
def defines functions. Types are written after :.
Pattern matching with | and match.
Recursion: Lean must check that it terminates, and it can when the recursive call uses a "smaller" argument (n instead of n + 1, xs instead of x :: xs).
inductive defines new types and structure defines records with fields.

Exercises: length, reverse and Tree.size.

Hint: for reverse, the ++ operator appends two lists.

Extra challenge: implement Tree.insert for a binary search tree and Tree.toList, which traverses it in order.

Solve them in the file, not here: the playground or VS Code shows the goal at each step. Tick an exercise once lake exe check marks it ✅ (or it compiles without sorry in the playground).

1`length`

Solved

/-- Returns the length of a list. -/
def length {α : Type} : List α → Nat
  | _ => sorry

3 tests check your definition when you run lake exe check Programming.

2`reverse`

Solved

/-- Reverses a list. -/
def reverse {α : Type} : List α → List α
  | _ => sorry

4 tests check your definition when you run lake exe check Programming.

3`Tree.size`

Solved

def Tree.size : Tree → Nat
  | _ => sorry

3 tests check your definition when you run lake exe check Programming.