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
|
