module Main where

{-@ type Even = {v:Int | v mod 2 = 0} @-}

{-@ weAreEven :: [Even] @-}
weAreEven     = [(0-10), (0-4), 0, 2, 666]

{-@ notEven :: Even @-}
notEven = 7

{-@ isEven :: n:Nat -> {v:Bool | (v <=> (n mod 2 == 0))} @-}
isEven   :: Int -> Bool
isEven 0 = True
isEven 1 = False
isEven n = not (isEven (n-1))

{-@ evens :: n:Nat -> [Even] @-}
evens n = [i | i <- range 0 n, isEven i]

{-@ range :: lo:Int -> hi:Int -> [{v:Int | (lo <= v && v < hi)}] / [hi -lo] @-}
range lo hi
  | lo < hi   = lo : range (lo+1) hi
  | otherwise = []

{-@ shift :: [Even] -> Even -> [Even] @-}
shift xs k = [x + k | x <- xs]

{-@ double :: [Nat] -> [Even] @-}
double xs = [x + x | x <- xs]



---

notEven    :: Int
weAreEven  :: [Int]
shift      :: [Int] -> Int -> [Int]
double     :: [Int] -> [Int]
range      :: Int -> Int -> [Int]

main = putStrLn "hello"