content: 
  {-@ LIQUID "--reflection" @-} 
  {-@ LIQUID "--ple"        @-} 
  
  module ReflectClient4 where
  
  import Language.Haskell.Liquid.ProofCombinators
  
  import ReflectLib4
  
  -- THIS IS NEEDED TO BRING THE NAMES INTO SCOPE FOR GHC ...
  forceImports = [ ]
  
  {-@ test1 :: {v:List a | v = Nil} @-}
  test1 :: List a
  test1 = Nil
  
  
  {-@ test2 :: {v:Proof | llen (Cons 1 Nil) = 1} @-}
  test2 :: Proof
  test2 =  llen (Cons 1 Nil)
        === 1 + llen Nil
        === 1
        *** QED
  
  {-@ test3 :: {v:Proof | llen (Cons 1 (Cons 2 Nil)) = 2} @-}
  test3 :: Proof
  test3 =  llen (Cons 1 (Cons 2 Nil))
        === 1 + llen (Cons 2 Nil)
        === 1 + 1 + llen Nil
        *** QED
  
  {-@ zen :: xs:List a -> {v:Nat | v = llen xs} @-}
  zen :: List a -> Int
  zen Nil        = 0
  zen (Cons h t) = 1 + zen t
  
  {-@ test5 :: { app (Cons 1 Nil) (Cons 2 (Cons 3 Nil)) = Cons 1 (Cons 2 (Cons 3 Nil)) } @-}
  test5 =   app (Cons 1 Nil) (Cons 2 (Cons 3 Nil))
        === Cons 1 (app Nil (Cons 2 (Cons 3 Nil)))
        === Cons 1 (Cons 2 (Cons 3 Nil))
        *** QED
  
  {-@ thmAppLen :: xs:List a -> ys:List a -> { llen (app xs ys) == llen xs + llen ys} @-}
  thmAppLen :: List a -> List a -> Proof
  thmAppLen Nil ys
    =  ()
  
  thmAppLen (Cons x xs) ys
    = thmAppLen xs ys
  