content: {-@ LIQUID "--reflection" @-}
  {-@ LIQUID "--ple" @-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  module Data.List where
  import Prelude hiding (id)
  
  import Data.Function
  
  {-@ data List a = Nil | Cons {lh::a, lt::List a} @-}
  data List a = Nil | Cons a (List a)
  
  {-@ reflect foldrList @-}
  foldrList :: (a -> b -> b) -> b -> List a -> b
  foldrList _ x Nil         = x
  foldrList f x (Cons y ys) = f y (foldrList f x ys)
  
  
  {-@ reflect foldlList @-}
  foldlList :: (b -> a -> b) -> b -> List a -> b
  foldlList _ x Nil         = x
  foldlList f x (Cons y ys) = foldlList f (f x y) ys
  
  
  {-@ reflect appendL @-}
  appendL :: List a -> List a -> List a
  appendL Nil         ys = ys
  appendL (Cons x xs) ys = Cons x (appendL xs ys)
  
  {-@ reflect appendLNil @-}
  {-@ appendLNil :: xs:List a -> {appendL xs Nil == xs} @-}
  appendLNil :: List a -> ()
  appendLNil Nil         = ()
  appendLNil (Cons x xs) = appendLNil xs
  
  {-@ reflect appendLAssoc @-}
  {-@ appendLAssoc :: xs:List a -> ys:List a -> zs:List a -> {appendL (appendL xs ys) zs == appendL xs (appendL ys zs)} @-}
  appendLAssoc :: List a -> List a -> List a -> ()
  appendLAssoc Nil         _  _  = ()
  appendLAssoc (Cons _ xs) ys zs = appendLAssoc xs ys zs
  
  {-@ reflect fmapList @-}
  fmapList :: (a -> b) -> List a -> List b
  fmapList f Nil = Nil
  fmapList f (Cons x xs) = Cons (f x) (fmapList f xs)
  
  
  {-@ fmapListId :: x:List a -> {fmapList id x == id x}  @-}
  fmapListId :: List a -> ()
  fmapListId Nil = ()
  fmapListId (Cons _ xs) = fmapListId xs
  
  {-@ fmapListComposition :: forall a b c. f:(b -> c) -> g:(a -> b) -> x:List a -> {fmapList (compose f g) x == compose (fmapList f) (fmapList g) x} @-}
  fmapListComposition :: forall a b c. (b -> c) -> (a -> b) -> List a -> ()
  fmapListComposition f g Nil = ()
  fmapListComposition f g (Cons _ xs) = fmapListComposition f g xs
  
  {-@ fmapListResAppend :: f:(a -> b) -> xs:List a -> ys:List a -> {fmapList f (appendL xs ys) == appendL (fmapList f xs) (fmapList f ys)} @-}
  fmapListResAppend :: (a -> b) -> List a -> List a -> ()
  fmapListResAppend f Nil         ys = ()
  fmapListResAppend f (Cons _ xs) ys = fmapListResAppend f xs ys
  