module Test () where

{-@ type OList a = [a]<{\fld v -> (v >= fld)}> @-}

{-@ foo :: (Ord a) => z:a -> OList a -> [{v:a | z <= v}] @-}
foo y xs = bar y xs

bar :: (Ord a) => a -> [a] -> [a]
bar y []     = []
bar y z@(x:xs) = case compare y x of 
                   EQ -> xs
                   GT -> bar y xs
                   LT -> x:xs