Basics

We have to start somewhere

Add Numbers

#eval 2 + 2

Lean is a compiled language, so it doesn't have a REPL
#eval means "evaluate this while compiling"`
Run with lean add_numbers.lean

Defining Values

def sum : Int := 2 + 2
#eval sum

def introduces a definition
Type specified after a colon
- Int is integer
Assignment uses :=

Strict Typing

def nope : Int := 2 + "two"

basics/strict_values.lean:1:18: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  HAdd Nat String Int

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Python won't let you do this either
But Lean's type system is more powerful and its checking is stricter

Guards

def language: String := "Lean"
#guard language.length == 4

#guard introduces code that is checked during compilation
Versus Python's assert, which is checked as the program runs

Formatting Strings

def name : String := "Jesse"
def count : Nat := 3
#eval s!"{name} has done {count} exercises"

"Jesse has done 3 exercises"

Use s!"…" to interpolate values in strings
- Like Python's f-strings

Lists

def names : List String := ["first", "second", "third"]
#eval s!"names has {names.length} elements"
#eval s!"element 0 of names is '{names[0]}'"

"names has 3 elements"
"element 0 of names is 'first'"

Type of list elements must be declared, and elements must all have the same type
- Next lesson shows how to handle mixed types
Index from 0
Use List.length to get number of elements
- Just like String.length earlier

Defining Simple Functions

def alwaysTheSame : Float :=
  42.0

#eval alwaysTheSame

42.000000

def double (value : Float) : Float :=
  2 * value

#eval double 3.0

6.000000

def multiply (left : Float) (right : Float) : Float :=
  left * right

#eval multiply 3 4

12.000000

Result of a function is the value of its last expression
- So no need for return
Note that there aren't parentheses in double 3.0

What's Actually Happening

def multiply (left : Int) (right : Int) : Int :=
  left * right

def temp := multiply 3

#eval temp 4

Every function actually takes only one argument
func a b defines a function that takes one argument…
…and returns a function that takes one argument
This is called currying
- Named after the mathematician Haskell Curry
- The inspiration for Python's functools.partial

Conditionals

def classify (n : Int) : String :=
  if n > 0 then "positive"
  else if n < 0 then "negative"
  else "zero"

#eval classify 5
#eval classify (-3)
#eval classify 0

"positive"
"negative"
"zero"

if/else if/else is an expression returning a value
This doesn't work because the function isn't guaranteed to return a string

def classify (n : Int) : String :=
  if n > 0 then "positive"

basics/conditional_incomplete.lean:3:0: error: unexpected end of input; expected 'else'

This doesn't work because the types are inconsistent

def classify (n : Int) : String :=
  if n > 0 then "positive"
  else 3

basics/conditional_inconsistent.lean:3:7: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  OfNat String 3
numerals are polymorphic in Lean, but the numeral `3` cannot be used in a context where the expected type is
  String
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

That's a hell of an error message…

Another Way to Do It

#eval match 3 with
 | 0 => "zero"
 | _ => "nonzero"

"nonzero"

Use match…with for pattern matching
Each alternative uses | and =>
Use _ as a catch-all

Recursion

def sumList (xs : List Int) : Int :=
  match xs with
  | []      => 0
  | x :: xs => x + sumList xs

#eval sumList [1, 3, 5]

Use :: to get the head and tail of a list
- Head is one element
- Tail is a list
As with conditional, must handle all alternatives
Lean checks that you done this have during compilation

Map, Filter, and Fold

def numbers : List Int := [1, 3, 5, 7]

-- map transforms every element
#eval numbers.map (fun val => val * 2)

-- filter keeps only matching elements
#eval numbers.filter (fun val => val >= 5)

-- foldl accumulates from the left
#eval numbers.foldl (fun left right => left + right) 0

[2, 6, 10, 14]
[5, 7]
16

Some patterns are so common that they're supported directly
fun args => expr is used for short anonymous functions like Python's lambda
map and filter do what their names suggest
foldl is "fold left" and must be given an initial value

Local Definitions

def circleArea (radius : Float) : Float :=
  let pi := 3.14159
  let rSquared := radius * radius
  pi * rSquared

#eval circleArea 2.0

12.566360

Use let to define local values
let names are only visible within their enclosing expression

Tuples

def pair : Int × Int := (10, 20)

#eval pair.1
#eval pair.2

def swap (p : Int × Int) : Int × Int :=
  let (x, y) := p
  (y, x)

#eval swap pair

10
20
(20, 10)

× separates the types of tuple elements (type \times in the editor)
Use .1 and .2 to access elements (no, not .0)
Use let (x, y) := p to extract both elements at once

Missing Values

def firstElement (xs : List Int) : Option Int :=
  match xs with
  | []     => Option.none
  | x :: _ => Option.some x

#eval firstElement [10, 20, 30]
#eval firstElement []

def firstOrZero (xs : List Int) : Int :=
  match firstElement xs with
  | Option.none   => 0
  | Option.some x => x

#eval firstOrZero [10, 20, 30]
#eval firstOrZero []

some 10
none
10
0

Lean uses Option instead of None
A function that might not return a value has return type Option SomeType
Option.some value wraps a value; Option.none signals absence
The compiler forces you to handle both cases
- Unlike Python, where forgetting to check for None is a runtime error

Structures

structure Point where
  x : Float
  y : Float

def origin : Point := { x := 0.0, y := 0.0 }
def here : Point := { x := 3.0, y := 4.0 }

#eval origin.x
#eval here.y

def distance (p : Point) : Float :=
  Float.sqrt (p.x * p.x + p.y * p.y)

#eval distance here

0.000000
4.000000
5.000000

structure groups related values under one name
- Like a Python data class or named tuple
Access fields with .fieldName
Create a value by listing field names with := inside {}

Checking and Updating

#check 123

structure Point where
  x : Float
  y : Float

def origin : Point := { x := 0.0, y := 0.0 }
#check origin

def elsewhere : Point := {origin with x := 1.0 }
#eval elsewhere

123 : Nat
origin : Point
{ x := 1.000000, y := 0.000000 }

#check checks the type of an expression without evaluating it
Nat is a natural (non-negative) number

Type Inference

-- Lean can infer the type from the value
def greeting := "hello"
def count := 42

#eval greeting
#eval count

-- Lean can infer the return type of a function
def double (val : Int) := val * 2

#eval double 7

"hello"
42
14

Lean can often figure out types
A string literal is a String, a whole number is usually an Int
Return types of functions can often be inferred from the body
You can always add type annotations for clarity, but don't have to

Idiomatic Lean

def numbers : List Int := [1, 3, 5, 7]

-- use · shorthand for simple lambdas
#eval numbers.map (· * 2)

-- use mathematical symbols
#eval numbers.filter (· ≥ 5)

-- each · matches a parameter in order
#eval numbers.foldl (· + ·) 0

[2, 6, 10, 14]
[5, 7]
16

Use · (a centered dot) to match parameters
- Which is a horrible usability decision
Type \cdot in the editor and \gt to get ≥
If there are multiple parameters, each · matches the next one
- Which is an even worse usability decision, but we're stuck with it

Exercises

Fix: Missing Else Branch

-- This function should return "positive", "negative", or "zero"
-- but it has a bug. Fix it.
def describe (n : Int) : String :=
  if n > 0 then
    "positive"
  else if n < 0 then
    "negative"

hint

The describe function doesn't handle the case when n is zero
The compiler will reject this: add the missing else branch

Fix: Non-Exhaustive Match

-- This function should return the first element of a list
-- or 0 if the list is empty. Fix the bug.
def firstOrZero (xs : List Int) : Int :=
  match xs with
  | x :: _ => x

hint

firstOrZero only handles the case where the list has at least one element
Add a branch for the empty list that returns 0

Fix: Unhandled Option

-- This function should extract a value from an Option
-- or return "missing" for Option.none. Fix the bug.
def getValue (opt : Option String) : String :=
  match opt with
  | Option.some s => s

hint

getValue only handles Option.some but not Option.none
Add a branch that returns "missing" when the option is none

Fix: Wrong Base Case

-- This function should return the product of all numbers in a list
-- but it always returns 0. Fix the bug.
def product (xs : List Int) : Int :=
  match xs with
  | [] => 0
  | x :: rest => x * product rest

hint

Multiplying by zero gives zero, so the base case [] => 0 breaks everything
What should the product of an empty list be? (Hint: think about 1 * 2 * 3)

Fix: Wrong Return Type

-- This function should return the sum of two integers
-- but the type annotation is wrong. Fix the bug.
def add (x : Int) (y : Int) : String :=
  x + y

hint

The function body returns an Int but the type annotation says String
Fix the type annotation to match what the body actually returns

Write: Double a Number

-- Write a function 'double' that multiplies a Float by 2.
def double (x : Float) : Float :=
  0.0

#guard double 3.0 == 6.0
#guard double (-1.5) == -3.0

hint

Replace 0.0 with an expression that doubles x
The #guard statements will tell you if your solution is correct

Write: Make a Greeting

-- Write a function 'greet' that returns s!"Hello, {name}!".
def greet (name : String) : String :=
  ""

#guard greet "World" == "Hello, World!"
#guard greet "Lean" == "Hello, Lean!"

hint

Replace "" with a string that includes the person's name
Use s!"…" interpolation like the examples earlier in the lesson

Write: List Length

-- Write a function 'myLength' that returns the length of a List Int
-- using recursion. Do not use List.length.
def myLength (xs : List Int) : Nat :=
  0

#guard myLength [] == 0
#guard myLength [1, 2, 3] == 3
#guard myLength [5] == 1

hint

Write a recursive function that counts the elements in a list
Do not use List.length — implement it yourself with match and ::

Write: Swap a Tuple

-- Write a function 'swap' that takes (Int, String)
-- and returns (String, Int) with the elements exchanged.
def swap (p : Int × String) : String × Int :=
  ("", 0)

#guard swap (42, "hello") == ("hello", 42)
#guard swap (7, "seven") == ("seven", 7)

hint

Replace ("", 0) with the elements of p in reverse order
Use .1 and .2 to access the fields of the tuple

Write: Update a Structure

structure Point where
  x : Float
  y : Float

-- Write a function 'moveRight' that takes a Point
-- and returns a new Point with x increased by 1.0.
def moveRight (p : Point) : Point :=
  p

#guard moveRight { x := 3.0, y := 0.0 } == { x := 4.0, y := 0.0 }
#guard moveRight { x := 0.0, y := 5.0 } == { x := 1.0, y := 5.0 }

hint

Replace p with a new Point that has x incremented by 1.0
Use the { old with field := newVal } syntax shown in the structures section