10
data List (A : Set) : Set where
12
_::_ : A -> List A -> List A
14
filter : {A : Set} -> (A -> Bool) -> List A -> List A
16
filter p (x :: xs) with p x
17
... | true = x :: filter p xs
18
... | false = filter p xs
22
data _⊆_ {A : Set} : List A -> List A -> Set where
24
drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
25
keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys
27
subset : {A : Set}(p : A -> Bool)(xs : List A) -> filter p xs ⊆ xs
29
subset p (x :: xs) with p x
30
... | true = keep (subset p xs)
31
... | false = drop (subset p xs)