Programming · 8 min

Lists and functions

List α is a list whose elements have type α. For example, List Nat holds natural numbers. List.map applies a function to each element and returns a new list.

fun n => n * 2 is an anonymous function. Lean can infer n’s type from the list you are mapping over. You can pass named functions to map as well.

Exercise

Make doubleAll double every number in its input list.

Open exercise in editor

def doubleAll (xs : List Nat) : List Nat :=
  xs

#eval doubleAll [1, 2, 3]

Hint

Use xs.map with the anonymous function fun n => n * 2.

Solution

def doubleAll (xs : List Nat) : List Nat :=
  xs.map (fun n => n * 2)

#eval doubleAll [1, 2, 3]

Related example

Lists & pipelines