/Prelude-v16.0.0/Optional/filter

Copy path to clipboard

Examples

filter Natural Natural/even (Some 2) ≡ Some 2
filter Natural Natural/odd (Some 2) ≡ None Natural

Source

{-
Only keep an `Optional` element if the supplied function returns `True`
-}
let filter
: ∀(a : Type) → (a → Bool) → Optional a → Optional a
= λ(a : Type)
→ λ(f : a → Bool)
→ λ(xs : Optional a)
→ ( λ(a : Type)
→ λ ( build
: ∀(optional : Type)
→ ∀(some : a → optional)
→ ∀(none : optional)
→ optional
)
build (Optional a) (λ(x : a) → Some x) (None a)
)
a
( λ(optional : Type)
→ λ(some : aoptional)
→ λ(none : optional)
→ merge
{ Some = λ(x : a) → if f x then some x else none, None = none }
xs
)

let example0 = assert : filter Natural Natural/even (Some 2) ≡ Some 2

let example1 = assert : filter Natural Natural/odd (Some 2) ≡ None Natural

in filter