diff --git a/perga.cabal b/perga.cabal
index a3f2c05..12515f1 100644
--- a/perga.cabal
+++ b/perga.cabal
@@ -1,13 +1,9 @@
 cabal-version:      3.0
 name:               perga
 
--- PVP summary:     +-+------- breaking API changes
---                  | | +----- non-breaking API additions
---                  | | | +--- code changes with no API change
 version:            0.1.0.0
 
--- A short (one-line) description of the package.
--- synopsis:
+synopsis: Basic proof assistant based on Calculus of Constructions
 
 -- A longer description of the package.
 -- description:
@@ -65,19 +61,3 @@ executable perga
     default-language:   Haskell2010
     default-extensions: OverloadedStrings
                       , GADTs
-
-test-suite tests
-    import:             warnings
-    type:               exitcode-stdio-1.0
-    main-is:            Tests.hs
-    other-modules:      ExprTests
-                      , CheckTests
-    build-depends:      base ^>=4.19.1.0
-                      , HUnit
-                      , text
-                      , containers
-                      , perga-lib
-    hs-source-dirs:     tests
-    default-language:   Haskell2010
-    default-extensions: OverloadedStrings
-                      , GADTs
diff --git a/tests/CheckTests.hs b/tests/CheckTests.hs
deleted file mode 100644
index 243c76e..0000000
--- a/tests/CheckTests.hs
+++ /dev/null
@@ -1,73 +0,0 @@
-module CheckTests (tests) where
-
-import Check
-import qualified Data.Map as M
-import Expr (Expr (..))
-import Test.HUnit
-
-sort :: Test
-sort = TestCase $ assertEqual "*" (Right Square) (checkType M.empty Star)
-
-freeVar :: Test
-freeVar =
-    TestCase $
-        assertEqual "{x = *} , [] |- x : □" (Right Square) (checkType (M.singleton "x" Star) (Free "x"))
-
-polyIdent :: Test
-polyIdent =
-    TestCase $
-        assertEqual
-            "fun (A : *) (x : A) . x"
-            (Right $ Pi "A" Star (Pi "" (Var 0 "A") (Var 1 "A")))
-            (checkType M.empty (Abs "A" Star (Abs "x" (Var 0 "A") (Var 0 "x"))))
-
-typeCons :: Test
-typeCons =
-    TestCase $
-        assertEqual
-            "fun (A B : *) . A -> B"
-            (Right $ Pi "" Star (Pi "" Star Star))
-            (checkType M.empty (Abs "A" Star (Abs "B" Star (Pi "" (Var 1 "A") (Var 1 "B")))))
-
-useTypeCons :: Test
-useTypeCons =
-    TestCase $
-        assertEqual
-            "fun (C : * -> *) (A : *) (x : C A) . x"
-            (Right $ Pi "C" (Pi "" Star Star) (Pi "A" Star (Pi "" (App (Var 1 "C") (Var 0 "A")) (App (Var 2 "C") (Var 1 "A")))))
-            (checkType M.empty $ Abs "C" (Pi "" Star Star) (Abs "A" Star (Abs "x" (App (Var 1 "C") (Var 0 "A")) (Var 0 "x"))))
-
-dependent :: Test
-dependent =
-    TestCase $
-        assertEqual
-            "fun (S : *) (x : S) . S -> S"
-            (Right $ Pi "S" Star (Pi "" (Var 0 "S") Star))
-            (checkType M.empty $ Abs "S" Star (Abs "x" (Var 0 "S") (Pi "" (Var 1 "S") (Var 2 "S"))))
-
-useDependent :: Test
-useDependent =
-    TestCase $
-        assertEqual
-            "fun (S : *) (P : S -> *) (x : S) . P x"
-            (Right $ Pi "S" Star (Pi "" (Pi "" (Var 0 "S") Star) (Pi "" (Var 1 "S") Star)))
-            (checkType M.empty $ Abs "S" Star (Abs "P" (Pi "" (Var 0 "S") Star) (Abs "x" (Var 1 "S") (App (Var 1 "P") (Var 0 "x")))))
-
-big :: Test
-big =
-    TestCase $
-        assertEqual
-            "fun (S : *) (P Q : S -> *) (H : forall (x : S), P x -> Q x) (G : forall (x : S), P x) (x : S) . H x (G x)"
-            (Right $ Pi "S" Star (Pi "P" (Pi "" (Var 0 "S") Star) (Pi "Q" (Pi "" (Var 1 "S") Star) (Pi "" (Pi "x" (Var 2 "S") (Pi "" (App (Var 2 "P") (Var 0 "x")) (App (Var 2 "Q") (Var 1 "x")))) (Pi "" (Pi "x" (Var 3 "S") (App (Var 3 "P") (Var 0 "x"))) (Pi "x" (Var 4 "S") (App (Var 3 "Q") (Var 0 "x"))))))))
-            (checkType M.empty $ Abs "S" Star (Abs "P" (Pi "" (Var 0 "S") Star) (Abs "Q" (Pi "" (Var 1 "S") Star) (Abs "H" (Pi "x" (Var 2 "S") (Pi "" (App (Var 2 "P") (Var 0 "x")) (App (Var 2 "Q") (Var 1 "x")))) (Abs "G" (Pi "x" (Var 3 "S") (App (Var 3 "P") (Var 0 "x"))) (Abs "x" (Var 4 "S") (App (App (Var 2 "H") (Var 0 "x")) (App (Var 1 "G") (Var 0 "x")))))))))
-
-tests :: Test
-tests =
-    TestList
-        [ TestLabel "sort" sort
-        , TestLabel "λ→" $ TestList [freeVar]
-        , TestLabel "λ2" polyIdent
-        , TestLabel "λω" $ TestList [typeCons, useTypeCons]
-        , TestLabel "λP2" $ TestList [dependent, useDependent]
-        , TestLabel "λC" big
-        ]
diff --git a/tests/ExprTests.hs b/tests/ExprTests.hs
deleted file mode 100644
index 0d06fe9..0000000
--- a/tests/ExprTests.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-module ExprTests (tests) where
-
-import Expr
-import Eval
-import Test.HUnit
-
-inner :: Expr
-inner = Abs "x" (Var 0 "A") $ App (Var 2 "f") (Var 0 "x")
-
-e1 :: Expr
-e1 = Abs "A" Star inner
-
-fFree :: Test
-fFree = TestCase $ assertBool "f free" $ occursFree 0 e1
-
-incE1 :: Test
-incE1 =
-    TestCase $
-        assertEqual
-            "incIndices e1"
-            ( Abs "A" Star $
-                Abs "x" (Var 0 "A") $
-                    App (Var 3 "f") (Var 0 "x")
-            )
-            (incIndices e1)
-
-after :: Expr
-after = Abs "x" (Var 2 "B") $ App (Var 1 "f") (Var 0 "x")
-
-substE1 :: Test
-substE1 =
-    TestCase $
-        assertEqual
-            "e1[A := B]"
-            after
-            (subst 0 (Var 2 "B") inner)
-
-tests :: Test
-tests =
-    TestList
-        [ TestLabel "fFree" fFree
-        , TestLabel "incE1" incE1
-        , TestLabel "substE1" substE1
-        ]
diff --git a/tests/Tests.hs b/tests/Tests.hs
deleted file mode 100644
index d0c8043..0000000
--- a/tests/Tests.hs
+++ /dev/null
@@ -1,18 +0,0 @@
-module Main where
-
-import qualified CheckTests as C
-import qualified ExprTests as E
-import qualified System.Exit as Exit
-import Test.HUnit
-
-tests :: Test
-tests =
-    TestList
-        [ TestLabel "ExprTests" E.tests
-        , TestLabel "CheckTests" C.tests
-        ]
-
-main :: IO ()
-main = do
-    result <- runTestTT tests
-    if failures result > 0 then Exit.exitFailure else Exit.exitSuccess