Commit afce490a authored by nx200's avatar nx200
Browse files

added more examples

parent d30f343f
......@@ -6,10 +6,10 @@ module Head where
and1 True x = x
and1 False x = False
{-# CONTRACT head1 :: {xs | not (null xs)} -> {r | not (null r)} #-}
{-# CONTRACT head1 :: {xs | not1 (null1 xs)} -> {x | True} #-}
-- {-# CONTRACT head1 :: {xs | not1 (null1 xs)} -> {r | r > 0} #-}
head1 :: [Int] -> [Int]
head1 (x:xs) = [x]
head1 :: [Int] -> Int
head1 (x:xs) = x
not1 True = False
not1 False = True
......@@ -17,7 +17,7 @@ not1 False = True
null1 [] = True
null1 xs = False
{-# CONTRACT f :: {x | x > 0 && x < 5} -> any #-}
{-# CONTRACT f :: {x | x > 0} -> any #-}
f :: Int -> Int
f x = x + 1
......@@ -25,7 +25,10 @@ f x = x + 1
{-# CONTRACT res2 :: any #-}
res2 = head1 [5]
{-# CONTRACT res3 :: {x | True} #-}
res3 = head1 [6]
res5 = head1 [2]
res4 = head1 []
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment