{-
`partition` divides a `List` of elements into those that satisfy a predicate
and those that do not
-}
let Partition
    : Type → Type
    = λ(a : Type) → { true : List a, false : List a }

let partition
    : ∀(a : Type) → (a → Bool) → List a → Partition a
    =   λ(a : Type)
      → λ(f : a → Bool)
      → λ(xs : List a)
      → List/fold
          a
          xs
          (Partition a)
          (   λ(x : a)
            → λ(p : Partition a)
            →       if f x

              then  { true = [ x ] # p.true, false = p.false }

              else  { true = p.true, false = [ x ] # p.false }
          )
          { true = [] : List a, false = [] : List a }

let example0 =
        assert
      :   partition Natural Natural/even [ 0, 1, 2, 3 ]
        ≡ { true = [ 0, 2 ], false = [ 1, 3 ] }

in  partition