liquidhaskell-0.8.10.7: tests/import/lib/Spec.hs
module Spec where
data Foo = FooDC Int
{-@ data Foo = FooDC {unfoo :: {v:Int | 0 < v }} @-}
{-@ measure cfun @-}
{-@ cfun :: Foo -> {v:Int | 0 < v} @-}
cfun :: Foo -> Int
cfun (FooDC x) = xmodule Spec where
data Foo = FooDC Int
{-@ data Foo = FooDC {unfoo :: {v:Int | 0 < v }} @-}
{-@ measure cfun @-}
{-@ cfun :: Foo -> {v:Int | 0 < v} @-}
cfun :: Foo -> Int
cfun (FooDC x) = x