{-@ LIQUID "--totality"                            @-}
{-@ LIQUID "--exact-data-con"                      @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

module ReflectClient4a where

import Language.Haskell.Liquid.ProofCombinators
import ReflectLib3

stupidity = [ undefined gapp ]

{- test1 :: { llen Nil == 0 } @-}
test1 = ()

{- test2 :: { llen (Cons 2 Nil) == 1 } @-}
test2 = ()

{- test3 :: { llen (Cons 1 (Cons 2 Nil)) == 2 } @-}
test3 = ()

{- test4 :: { app Nil Nil == Nil } @-}

{-@ test4 :: { gapp Nil = Nil } @-}
test4 = ()


-- {- thmAppLen :: xs:List a -> ys:List a ->
      -- { llen (app xs ys) == llen xs + llen ys}
  -- @-}
-- thmAppLen :: List a -> List a -> Proof
-- thmAppLen Nil         ys = trivial
-- thmAppLen (Cons x xs) ys = thmAppLen xs ys