@@ -0,0 +1,19 @@
1+> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect alpha n) -> Bool
2+> isAnyBy _ (_ ** Nil) = False
3+> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)
4+
5+
6+> filterTagP : (p : alpha -> Bool) ->
7+> (as : Vect alpha n) ->
8+> so (isAnyBy p (n ** as)) ->
9+> (m : Nat ** (Vect (a : alpha ** so (p a)) m, so (m > O)))
10+> filterTagP p (a :: as) q with (p a)
11+> | True = (_
12+> **
13+> ((a ** believe_me oh)
14+> ::
15+> (fst (getProof (filterTagP p as (believe_me oh)))),
16+> oh
17+> )
18+> )
19+> | False = filterTagP p as (believe_me oh)