-- Test for operations that should be successfully verified.

id :: a -> a
id x = x

-- Booleans

myTrue = True

myBool = False ? True

myNot False = True
myNot True  = False

solve True = True

solveMyTrue = solve myTrue

andp False _ = False
andp True True = True
andp True False = False

andp2 = andp myBool myBool


-- Lists (structured data)

myhead (x:xs) = x

null []    = True
null (_:_) = False

f xs = case null xs of
         True -> True
         False -> myhead xs

-- Base types and literals

k 0 = 'a'
k 1 = 'b'

j = k (0?1)

-- Example for unreachable branches


unreachBranch x =
  case x of True -> case x of False -> solve x
                              True  -> solve x