liquidhaskell-0.7.0.0: tests/pos/bool0.hs
module BoolMeasure where
{-@ myhead :: {v:[a] | nonEmpty v} -> a @-}
myhead (x:_) = x
{-@ measure nonEmpty @-}
nonEmpty :: [a] -> Bool
nonEmpty (x:xs) = True
nonEmpty [] = False
module BoolMeasure where
{-@ myhead :: {v:[a] | nonEmpty v} -> a @-}
myhead (x:_) = x
{-@ measure nonEmpty @-}
nonEmpty :: [a] -> Bool
nonEmpty (x:xs) = True
nonEmpty [] = False