liquidhaskell-0.4.0.0: tests/pos/Mod1.hs
module Mod1 where
data Goo = G Int
{-@ measure myg :: Mod1.Goo -> Int
myg (Mod1.G n) = n
@-}
{-@ inc :: x:Goo -> {v: Goo | (myg v) > (myg x)} @-}
inc (G x) = G (x + 1)
module Mod1 where
data Goo = G Int
{-@ measure myg :: Mod1.Goo -> Int
myg (Mod1.G n) = n
@-}
{-@ inc :: x:Goo -> {v: Goo | (myg v) > (myg x)} @-}
inc (G x) = G (x + 1)