Map an optional value

1/4 ~12 minlean

Define `mapOption` by pattern matching.

3 lines · Lean 4

def mapOption (f : α → β) : Option α → Option β
  | none => sorry
  | some x => sorry

Objectifs

Indices

Voir la solution

def mapOption (f : α → β) : Option α → Option β
  | none => none
  | some x => some (f x)