Bool, q :: a -> Bool -> Bool>.
{y::a, flag :: {v:Bool | v} |- {v:a | v = y} <: a

}
(x:a -> Bool) -> [a] -> [a

] @-} filter f (x:xs) | f x = x : filter f xs | otherwise = filter f xs filter _ [] = [] {-@ isPos :: x:Int -> {v:Bool | v <=> x > 0} @-} isPos :: Int -> Bool isPos n = n > 0 {-@ isNeg :: x:Int -> {v:Bool | v <=> x < 0} @-} isNeg :: Int -> Bool isNeg n = n < 0 -- Now the below *should* work with -- p := \v -> 0 < v -- q := \x v -> v <=> 0 < 0 {-@ positives :: [Int] -> [{v:Int | v > 0}] @-} positives xs = filter isPos xs {-@ negatives :: [Int] -> [{v:Int | v < 0}] @-} negatives xs = filter isNeg xs {-@ positivesBAD :: [Int] -> [{v:Int | v < 0}] @-} positivesBAD xs = filter isPos xs