summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Positivity/Tests.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Positivity/Tests.hs')
-rw-r--r--src/full/Agda/TypeChecking/Positivity/Tests.hs27
1 files changed, 0 insertions, 27 deletions
diff --git a/src/full/Agda/TypeChecking/Positivity/Tests.hs b/src/full/Agda/TypeChecking/Positivity/Tests.hs
deleted file mode 100644
index 8efeb9d..0000000
--- a/src/full/Agda/TypeChecking/Positivity/Tests.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-
-module Agda.TypeChecking.Positivity.Tests where
-
-import Test.QuickCheck
-
-import Agda.TypeChecking.Positivity
-
-import Agda.Utils.SemiRing
-
--- | The 'oplus' method for 'Occurrence' matches that for 'Edge'.
-
-prop_oplus_Occurrence_Edge :: Edge -> Edge -> Bool
-prop_oplus_Occurrence_Edge e1@(Edge o1 _) e2@(Edge o2 _) =
- case oplus e1 e2 of
- Edge o _ -> o == oplus o1 o2
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under GHC 7.8.
-return []
-
--- | Tests.
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.TypeChecking.Positivity"
- $quickCheckAll