module ListRange () where
import Language.Haskell.Liquid.Prelude
data List a = Nil | Cons a (List a)
-- isOdd x = not (isEven x)
-- isEven x = not (isOdd x)
-- foo x = x+1
insert y Nil
= Cons y Nil
insert y (Cons x xs) | (y <= x)
= let ys1 = Cons x xs in
let ys2 = Cons y ys1 in ys2
insert y (Cons x xs) | (x < y)
= let xs1 = insert y xs in
let xs2 = Cons x xs1 in xs2
chk2 y =
case y of
Nil -> True
Cons x1 xs -> case xs of
Nil -> True
Cons x2 xs2 -> liquidAssertB (x1 == x2) && chk2 xs2
n, m :: Int
n = choose 0
m = choose 0
-- bar = insert n (range 2 8)
bar = insert n (insert m Nil)
range l h = if l <=h then Cons l (range (l+1) h) else Nil
mkList :: [a] -> List a
mkList = foldr Cons Nil
prop0 = chk2 bar