summaryrefslogtreecommitdiff
path: root/testsuite/tests/esc/TestImport.hs
blob: bf91eafb6336c380b0e2d981d759b802094c5bae (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
module TestImport where

import TestList

{-# CONTRACT t2 :: _ #-}
t2 = head1 [True]  -- same as TestList res2

{-# CONTRACT t3 :: {x | True} #-}
t3 = head1 [True]  -- same as TestList.res3

t4 = head1 []      -- same as TestList.res4

t5 = head1 [True]  -- same as TestList.res5

t2a = res2
t3a = res3
t4a = res4
t5a = res5

{-# CONTRACT tail1 :: {xs | not1 (null1 xs)} ->  {r | True} #-}
tail1 :: [Int] -> [Int]
tail1 (x:xs) = xs

{-# CONTRACT tail2 :: {xs | not (null xs)} ->  {r | True} #-}
tail2 :: [Int] -> [Int]
tail2 (x:xs) = xs