diff --git a/tests/Main.idr b/tests/Main.idr
index 9cad4e9..37ebb11 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -32,7 +32,8 @@ idrisTests
        "interface005",
        "import001", "import002",
        "lazy001",
-       "record001", "record002"]
+       "record001", "record002",
+       "total001", "total002", "total003"]
 
 chdir : String -> IO Bool
 chdir dir 
diff --git a/tests/idris2/total001/Total.idr b/tests/idris2/total001/Total.idr
new file mode 100644
index 0000000..df266dd
--- /dev/null
+++ b/tests/idris2/total001/Total.idr
@@ -0,0 +1,17 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+data Fin : Nat -> Type where
+     FZ : Fin (S k)
+     FS : Fin k -> Fin (S k)
+
+lookup : Fin n -> Vect n a -> a
+lookup FZ (x :: xs) = x
+lookup (FS k) (x :: xs) = lookup k xs
+
+lookup' : Fin n -> Vect n a -> a
+lookup' (FS k) (x :: xs) = lookup' k xs
+
+lookup'' : Fin n -> Vect n a -> a
+lookup'' n xs = lookup' n xs
diff --git a/tests/idris2/total001/expected b/tests/idris2/total001/expected
new file mode 100644
index 0000000..f0f3eb4
--- /dev/null
+++ b/tests/idris2/total001/expected
@@ -0,0 +1,7 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.lookup: All cases covered
+Main> Main.lookup':
+lookup' FZ _
+Main> Main.lookup'': Calls non covering function Main.lookup'
+Main> Bye for now!
diff --git a/tests/idris2/total001/input b/tests/idris2/total001/input
new file mode 100644
index 0000000..1412c9d
--- /dev/null
+++ b/tests/idris2/total001/input
@@ -0,0 +1,4 @@
+:missing lookup
+:missing lookup'
+:missing lookup''
+:q
diff --git a/tests/idris2/total001/run b/tests/idris2/total001/run
new file mode 100755
index 0000000..9005d19
--- /dev/null
+++ b/tests/idris2/total001/run
@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build
diff --git a/tests/idris2/total002/Total.idr b/tests/idris2/total002/Total.idr
new file mode 100644
index 0000000..58a1481
--- /dev/null
+++ b/tests/idris2/total002/Total.idr
@@ -0,0 +1,13 @@
+data Fin : Nat -> Type where
+     FZ : Fin (S k)
+     FS : Fin k -> Fin (S k)
+
+noFinZ : Fin Z -> Void
+noFinZ FZ impossible
+noFinZ (FS k) impossible
+
+noFinZ' : Fin Z -> Void
+noFinZ' x impossible
+
+noEmpty : Void -> Fin Z
+noEmpty t impossible
diff --git a/tests/idris2/total002/expected b/tests/idris2/total002/expected
new file mode 100644
index 0000000..21dc194
--- /dev/null
+++ b/tests/idris2/total002/expected
@@ -0,0 +1,6 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.noFinZ: All cases covered
+Main> Main.noFinZ': All cases covered
+Main> Main.noEmpty: All cases covered
+Main> Bye for now!
diff --git a/tests/idris2/total002/input b/tests/idris2/total002/input
new file mode 100644
index 0000000..93e4a70
--- /dev/null
+++ b/tests/idris2/total002/input
@@ -0,0 +1,4 @@
+:missing noFinZ
+:missing noFinZ'
+:missing noEmpty
+:q
diff --git a/tests/idris2/total002/run b/tests/idris2/total002/run
new file mode 100755
index 0000000..9005d19
--- /dev/null
+++ b/tests/idris2/total002/run
@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build
diff --git a/tests/idris2/total003/Total.idr b/tests/idris2/total003/Total.idr
new file mode 100644
index 0000000..03278e6
--- /dev/null
+++ b/tests/idris2/total003/Total.idr
@@ -0,0 +1,25 @@
+onlyOne : Int -> Int
+onlyOne 1 = 2
+
+covered : Int -> Int
+covered 1 = 2
+covered 2 = 3
+covered _ = 94
+
+data IntNat : Integer -> Nat -> Type where
+     IsZero : IntNat 0 Z
+     IsSuc : IntNat 1 (S k)
+
+-- Only identified as covering if 'x' has multiplicity 0 because then it
+-- doesn't show up in the case tree!
+matchInt : (0 x : Integer) -> (n : Nat) -> IntNat x n -> String
+matchInt 0 Z IsZero = "Zero"
+matchInt 1 (S k) IsSuc = "Non Zero"
+
+-- Should be identified as covering but isn't yet since the checker requires
+-- a catch all case. This does at least test that the declared 'impossible'
+-- case really is impossible; we can update it when the checker improves!
+matchInt' : (x : Integer) -> (n : Nat) -> IntNat x n -> String
+matchInt' 0 Z IsZero = "Zero"
+matchInt' 1 (S k) IsSuc = "Non Zero"
+matchInt' 0 (S k) x impossible
diff --git a/tests/idris2/total003/expected b/tests/idris2/total003/expected
new file mode 100644
index 0000000..e21b9bd
--- /dev/null
+++ b/tests/idris2/total003/expected
@@ -0,0 +1,10 @@
+1/1: Building Total (Total.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> Main.onlyOne:
+onlyOne _
+Main> Main.covered: All cases covered
+Main> Main.matchInt: All cases covered
+Main> Main.matchInt':
+matchInt' _ _ IsZero
+matchInt' _ _ IsSuc
+Main> Bye for now!
diff --git a/tests/idris2/total003/input b/tests/idris2/total003/input
new file mode 100644
index 0000000..39f99a2
--- /dev/null
+++ b/tests/idris2/total003/input
@@ -0,0 +1,5 @@
+:missing onlyOne
+:missing covered
+:missing matchInt
+:missing matchInt'
+:q
diff --git a/tests/idris2/total003/run b/tests/idris2/total003/run
new file mode 100755
index 0000000..9005d19
--- /dev/null
+++ b/tests/idris2/total003/run
@@ -0,0 +1,3 @@
+$1 Total.idr < input
+
+rm -rf build