fold? は有用か

[Seasawher]

そもそもfoldとOptionの組み合わせで書けるのか？

[Seasawher]

実装するとしたらこういう感じ

head? を取ってきて init に渡せば foldrM とかで書けるような気もする

universe u v
variable {α : Type u} {β : Type v}

def List.foldr? (f : α → α → α) : List α → Option α
  | [] => none
  | a :: as =>
    match foldr? f as with
    | none => some a
    | some b => some (f a b)

#guard [13, 12, 3, 6].foldr? (min · ·) = some 3
#guard [1, 2, 3, 4].foldr? (· + ·) = some 10
#guard ([] : List Nat).foldr? (max · ·) = none