【Lean4】Option

Option

値が存在するかもしれないし、存在しないかもしれない場合に使う

Plaintext

def safeHead (xs : List Nat) : Option Nat :=
  match xs with
  | [] => none
  | x :: _ => some x

def safeHead (xs : List Nat) : Option Nat :=
  match xs with
  | [] => none
  | x :: _ => some x