λleanlab

Programs

Lists & pipelines

Build a small data pipeline with immutable lists and higher-order functions.

Open Lists.lean in editor
def scores : List Nat := [12, 7, 24, 3, 18]

def main : IO Unit := do
  let doubled := scores.map (fun n => n * 2)
  let high := scores.filter (fun n => n > 10)
  let total := scores.foldl (fun acc n => acc + n) 0
  IO.println s!"Doubled: {doubled}"
  IO.println s!"Above 10: {high}"
  IO.println s!"Total: {total}"

Explanation

List Nat

A list whose elements all have type Nat. Types can themselves take parameters.

fun n =>

An anonymous function, useful when passing behavior into map or filter.

let

Introduces a local value. Lean usually infers its type from the expression.

Expected output

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

Doubled: [24, 14, 48, 6, 36]
Above 10: [12, 24, 18]
Total: 64

Exercise

Change the filter to keep scores above 15.