module ListRange (llen) where import Language.Haskell.Liquid.Prelude {-@ data List [llen] a
x1:a -> Bool> = Nil | Cons { lHd :: a, lTl :: List
(a
) }
@-}
{-@ measure llen @-}
llen :: (List a) -> Int
{-@ llen :: List a -> Nat @-}
llen Nil = 0
llen (Cons x xs) = 1 + (llen xs)
{-@ 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