packages feed

liquidhaskell-0.8.10.7: tests/measure/neg/GList00Lib.hs

module GList00Lib where 

{-@ die :: {v: () | false} -> a @-}
die :: () -> a
die = undefined 

{-@ safeHead :: {v:[a] | 0 <= llen v} -> a @-} 
safeHead :: [a] -> a 
safeHead (x:_) = x 
safeHead []    = die () 

{-@ measure llen @-}
{-@ llen :: [a] -> Nat @-}
llen :: [a] -> Int
llen []     = 0 
llen (x:xs) = 1 + llen xs