Lists and missing values
Lists, their two shapes, and Option for a value that may be absent.
In this course 10 / 11
A List Nat is a sequence of numbers: [5, 8, 2], or the empty list []. Lists come with many functions:
#eval [5, 8, 2].length
#eval [5, 8, 2].reverse
#eval [1, 2] ++ [3]3 [2, 8, 5] [1, 2, 3]
Asking for the first element is trickier: the empty list has none. So head? returns an Option Nat, which is either some n (here is a value) or none (there is no value):
#eval [5, 8, 2].head?
#eval ([] : List Nat).head?some 5 none
A list is an inductive type with two shapes: empty, [], or a first element followed by the rest, written x :: rest. So you can pattern match on a list just as on Mode. To match on a value inside a function body, write match … with:
def describe (o : Option Nat) : String :=
match o with
| some _ => "a value"
| none => "nothing"Worked example
def firstOrZero : List Nat → Nat
| [] => 0
| x :: _ => x
#eval firstOrZero [7, 8] -- 7
#eval firstOrZero [] -- 0
#eval firstOrZero [0] -- 0, the same answer as for []The last two answers are both 0, so a caller cannot tell an empty list from a list that starts with zero. Option keeps that difference: none versus some 0.
Lists are empty or x :: rest, and you can match on those shapes. Option says “maybe there is a value”: some x or none.
Write firstItem : List Nat → Option Nat by pattern matching: none for the empty list, and some x for a list that starts with x.
Suggested steps
- Give firstItem the type List Nat → Option Nat
- Handle the empty list
- Handle a list with a first element
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
example : firstItem [] = none := by rfl example : firstItem [4, 1] = some 4 := by rfl example : firstItem [0] = some 0 := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct