blob: 24b035ccc1bd8acdded549ba33fd722fb2107d8b (
plain)
1
2
3
4
5
6
7
8
9
10
|
{-# TYPE nat = {x | x > 0} #-}
{-# TYPE notNull = {xs | not (null xs)} #-}
{-# CONTRACT f :: nat -> nat #-}
f :: Int -> Int
f x = x
{-# CONTRACT g :: notNull -> any #-}
g :: [Int] -> Int
g (x:xs) = x
|