liquidhaskell-0.8.6.0: tests/pos/state00.hs
module StateMonad () where
type State = Int
data ST a b = Superb (b -> (a, b))
{-@ fresh :: ST {v:Int | v >= 0} {v:Int | v >= 0} @-}
fresh :: ST Int Int
fresh = Superb (\n -> (n, n+1))
module StateMonad () where
type State = Int
data ST a b = Superb (b -> (a, b))
{-@ fresh :: ST {v:Int | v >= 0} {v:Int | v >= 0} @-}
fresh :: ST Int Int
fresh = Superb (\n -> (n, n+1))