diff options
Diffstat (limited to 'testsuite/tests/esc/TestList.hs')
-rw-r--r-- | testsuite/tests/esc/TestList.hs | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/testsuite/tests/esc/TestList.hs b/testsuite/tests/esc/TestList.hs new file mode 100644 index 0000000000..66f9df2263 --- /dev/null +++ b/testsuite/tests/esc/TestList.hs @@ -0,0 +1,24 @@ +module TestList where + +{-# CONTRACT head1 :: {ys | not1 (null1 ys)} -> {r | True} #-} +-- {-# CONTRACT head1 :: {xs | not (null xs)} -> {r | True} #-} +head1 :: [Bool] -> Bool +head1 (x:xs) = x + +not1 True = False +not1 False = True + +null1 [] = True +null1 xs = False + +{-# CONTRACT res2 :: _ #-} +res2 = head1 [True] + +{-# CONTRACT res3 :: {x | True} #-} +res3 = head1 [True] + +res4 = head1 [] + +res5 = head1 [True] + + |