blob: 2b9ee29688440705a65eda90d6d4f0885d626160 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
module Sum where
{-- {-# SPECIALISE f :: Int -> Int #-}
-- {-# CONTRACT f :: x:{y | y > 0} -> {r | r == x + 1} #-}
-- {-# CONTRACT f :: x:{y | y > 0} -> {y | y > 0} -> {r | r == x + 1} #-}
-- {-# CONTRACT f :: any -> {y | y > 0} #-}
-- {-# CONTRACT f :: {y | y > 0} -> _ #-}
{-# CONTRACT inc :: {y | y > 0} -> {r | r > 1} #-}
inc :: Int -> Int
inc x = x + 1
-}
-- {-# CONTRACT sum2 :: x:{y | y > 0} -> {y | y > x} -> {r | r > 0} #-}
-- {-# CONTRACT sum2 :: x:{y | y > 0} -> {y | y > x} -> _ #-}
sum2 :: Int -> Int -> Int
sum2 x y = x + y
{-
t1 = inc 5
t2a = sum2 (inc 5) 2
t2b = sum2 (inc 5) 6
-}
|
