blob: 810599b033d6c8211ed288fd392e8d99e503483f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
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
|