filter

{-
Only keep elements of the list where the supplied function returns `True`

Examples:

```
./filter Natural Natural/even ([+2, +3, +5] : List Natural)
= [ +2 ] : List Natural

./filter Natural Natural/odd ([+2, +3, +5] : List Natural)
= [ +3, +5 ] : List Natural
```
-}
    let filter
        : ∀(a : Type) → (a → Bool) → List a → List a
        =   λ(a : Type)
          → λ(f : a → Bool)
          → λ(xs : List a)
          → List/build
            a
            (   λ(list : Type)
              → λ(cons : a → list → list)
              → List/fold
                a
                xs
                list
                (λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)
            )

in  filter