Forgot to add some test files!

tests/idris2/total007/expected

@@ -0,0 +1,5 @@
+1/1: Building partial (partial.idr)
+partial.idr:5:1--7:1:foo is not covering. Missing cases:
+	foo Nothing
+partial.idr:13:1--15:1:qsortBad is not total:
+	possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad

tests/idris2/total007/partial.idr

@@ -0,0 +1,29 @@
+import Data.List
+
+-- %default total
+
+total
+foo : Maybe a -> a
+foo (Just x) = x
+
+total
+bar : %World -> ()
+bar %MkWorld = ()
+
+total
+qsortBad : Ord a => List a -> List a
+qsortBad [] = []
+qsortBad (x :: xs)
+   = qsortBad (filter (< x) xs) ++ x :: qsortBad (filter (> x) xs)
+
+total
+qsort : Ord a => List a -> List a
+qsort [] = []
+qsort (x :: xs)
+   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
+         x :: qsort (assert_smaller (x :: xs) (filter (> x) xs))
+
+partial
+main : IO ()
+main = do let x = foo Nothing
+          printLn (the Int x)

tests/idris2/total007/run

@@ -0,0 +1,3 @@
+$1 --no-banner partial.idr --check
+
+rm -rf build