/Prelude-v19.0.0/Optional/filter.dhall

Copy path to clipboard

Only keep an Optional element if the supplied function returns True

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