blob: 66f9df2263ad4adb4b7b3059b98f2eac5c9a919c (
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
|
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]
|
