module T () where

import Language.Haskell.Liquid.Prelude

{-@ assert zipW :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len(v) = len(xs)} -> {v : [c] | len(v) = len(xs)} @-}
zipW :: (a->b->c) -> [a]->[b]->[c]
zipW f (a:as) (b:bs) = f a b : zipW f as bs
zipW _ [] []         = []
zipW _ [] (_:_)      = liquidError "zipWith1"
zipW _ (_:_) []      = liquidError "zipWith1"

{-@ assert foo :: (a -> b -> c) -> xs : [a] -> ys:{v:[b] | len(v) = len(xs)} -> {v : [c] | len(v) = len(xs)} @-}
foo = zipW