liquidhaskell-0.4.0.0: tests/pos/LocalSpec0.hs
module LocalSpec0 (foo) where
{-@ foo :: x:Int -> {v:Int | v > x } @-}
foo :: Int -> Int
foo x = go x
{-@ go :: n:Int -> {v:Int | v = n + 1} @-}
go :: Int -> Int
go x = x + 1
module LocalSpec0 (foo) where
{-@ foo :: x:Int -> {v:Int | v > x } @-}
foo :: Int -> Int
foo x = go x
{-@ go :: n:Int -> {v:Int | v = n + 1} @-}
go :: Int -> Int
go x = x + 1