let filterOptional
: ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b
= λ(a : Type)
→ λ(b : Type)
→ λ(f : a → Optional b)
→ λ(l : List a)
→ List/build
b
( λ(list : Type)
→ λ(cons : b → list → list)
→ λ(nil : list)
→ List/fold
a
l
list
( λ(x : a)
→ λ(xs : list)
→ Optional/fold b (f x) list (λ(opt : b) → cons opt xs) xs
)
nil
)
in filterOptional