liquidhaskell-0.4.0.0: tests/neg/StreamInvariants.hs
module Invariant where
{-@ using [a] as {v : [a] | (len v) > 0 } @-}
xs = []
add x xs = x:xs
bar xs = head xs
foo xs = tail xs
module Invariant where
{-@ using [a] as {v : [a] | (len v) > 0 } @-}
xs = []
add x xs = x:xs
bar xs = head xs
foo xs = tail xs