fix name clashes in tests

ucsd-progsys · Apr 20, 2016 · 6386a0e · 6386a0e
1 parent 37764d3
commit 6386a0e
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 7 deletions.
diff --git a/tests/pos/data2.hs b/tests/pos/data2.hs
@@ -3,8 +3,8 @@ module Range (prop_rng1) where
 import Control.Applicative
 import Language.Haskell.Liquid.Prelude
 
-data LL a = N | C { head :: a, tail :: (LL a) }
-{-@ data LL [llen] a = N | C { head :: a, tail :: (LL a) } @-}
+data LL a = N | C { headC :: a, tailC :: (LL a) }
+{-@ data LL [llen] a = N | C { headC :: a, tailC :: (LL a) } @-}
 
 {-@ measure llen :: (LL a) -> Int
     llen(N)      = 0

diff --git a/tests/pos/dropwhile.hs b/tests/pos/dropwhile.hs
@@ -66,9 +66,6 @@ dropWhile f Emp  = Emp
 witness :: Eq a => (a -> Bool) -> (a -> Bool -> Bool) -> a -> Bool -> a -> Bool
 witness p w = \ y b v -> (not b) ==> w y b ==> (v == y) ==> p v
 
-{-@ measure tail :: forall a. { es : [a] | len es >= 1 } -> [a] @-}
-tail :: [a] -> [a]
-tail = undefined
 -------------------------------------------------------------------------------
 -- | Drop elements until you hit a `3`
 -------------------------------------------------------------------------------

diff --git a/tests/pos/stacks0.hs b/tests/pos/stacks0.hs
@@ -4,8 +4,8 @@ import Data.Set (Set(..))
 
 data LL a = Nil | Cons { head :: a, tail :: LL a }
 
-{-@ data LL a = Nil | Cons { head :: a 
-                           , tail :: {v: LL a | not (Set_mem head (elts v))  } } 
+{-@ data LL a = Nil | Cons { headC :: a
+                           , tailC :: {v: LL a | not (Set_mem headC (elts v))  } }
   @-}
 
 {-@ measure elts :: LL a -> (Set a)