liquidhaskell-0.9.0.2.1: tests/pos/Spec0.hs

module Spec0 () where

import Language.Haskell.Liquid.Prelude

{-@ assert incr :: x:{v: Int | v >= 0} -> {v: Int | v > x} @-}
incr   :: Int -> Int
incr x = x + 1

myabs x = if x >= 0 then incr x else (0 - x)

prop_abs   = let n1 = choose 0 in
             liquidAssertB ((myabs n1) >= 0)