Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.


import Data.Vect

partition_condition : (f : elem -> Bool) -> (v : Vect n elem) -> Type
partition_condition {n} f v =
  case partition f v of
    ((z1 ** pt), (z2 ** pf)) => z1 + z2 = n

partition_length : (f : elem -> Bool) -> (v : Vect n elem) -> partition_condition f v
partition_length f [] = Refl
partition_length f (x :: xs) with (partition_length f xs)
  | IH with (partition f xs)
    | ((p ** vt), (q ** vf)) with (f x)
      | False =
        rewrite sym (plusSuccRightSucc p q) in
        rewrite IH in Refl
      | True =
        rewrite IH in Refl