module ListRange () where import Language.Haskell.Liquid.Prelude {-@ data List [llen] a
x1:a -> Bool> = Nil | Cons { lHd :: a, lTl :: List
(a
) }
@-}
{-@ measure llen :: (List a) -> Int
llen(Nil) = 0
llen(Cons x xs) = 1 + (llen xs)
@-}
{-@ invariant {v:List a | (llen v) >= 0} @-}
{-@ qualif ZLLen(v:ListRange.List a) : (llen(v) >= 0)@-}
{-@ qualif CmpLLen(v:ListRange.List a, a:ListRange.List b) : (llen v <= llen a) @-}
data List a = Nil | Cons a (List a)
append k Nil ys = Cons k ys
append k (Cons x xs) ys = Cons x (append k xs ys)
takeL x Nil = Nil
takeL x (Cons y ys) = if (y