git.iko.soy/Idris-dev
on master help sign in
Add tests for #4282 and #4299
a6d701aIlya Yanok
test/TestData.hs+3−1
compare with master
unifiedsplit
@@ -319,7 +319,9 @@ testFamiliesData = [
319 ( 20, ANY ),
319 ( 20, ANY ),
320 ( 21, ANY ),
320 ( 21, ANY ),
321 ( 22, ANY ),
321 ( 22, ANY ),
322− ( 23, ANY )]),
322+ ( 23, ANY ),
323+ ( 25, ANY ),
324+ ( 26, ANY )]),
323 ("tutorial", "Tutorial examples",
325 ("tutorial", "Tutorial examples",
324 [ ( 1, ANY ),
326 [ ( 1, ANY ),
325 ( 2, ANY ),
327 ( 2, ANY ),
test/totality025/expectednew file+18
@@ -0,0 +1,18 @@
1+totality025.idr:3:17-26:
2+ |
3+3 | bad1 _ _ _ Refl impossible
4+ | ~~~~~~~~~~
5+bad1 _ _ _ Refl is a valid case
6+
7+totality025.idr:12:17-26:
8+ |
9+12 | bad2 _ _ _ Refl impossible
10+ | ~~~~~~~~~~
11+bad2 _ _ _ Refl is a valid case
12+
13+totality025.idr:16:19-28:
14+ |
15+16 | bad3 _ _ _ _ Refl impossible
16+ | ~~~~~~~~~~
17+bad3 _ _ _ _ Refl is a valid case
18+
test/totality025/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ totality025.idr --check
3+rm -f *.ibc
test/totality025/totality025.idrnew file+17
@@ -0,0 +1,17 @@
1+total
2+bad1 : (f : Type -> Type) -> (x, y : Type) -> f x = f y -> Void
3+bad1 _ _ _ Refl impossible
4+
5+total
6+ohoh : Void
7+ohoh = bad1 id Unit Unit Refl
8+
9+-- of course, these shouldn't be provable as well:
10+total
11+bad2 : (f, g : Type -> Type) -> (x : Type) -> f x = g x -> Void
12+bad2 _ _ _ Refl impossible
13+
14+total
15+bad3 : (f, g : Type -> Type) -> (x, y : Type) -> f x = g y -> Void
16+bad3 _ _ _ _ Refl impossible
17+
test/totality026/expectednew file+6
@@ -0,0 +1,6 @@
1+totality026.idr:5:8-17:
2+ |
3+5 | p Here impossible
4+ | ~~~~~~~~~~
5+p Here is a valid case
6+
test/totality026/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ totality026.idr --check
3+rm -f *.ibc
test/totality026/totality026.idrnew file+7
@@ -0,0 +1,7 @@
1+import Data.Vect
2+
3+total
4+p : Elem (Maybe x) (map Maybe xs) -> Elem x xs
5+p Here impossible
6+p (There l) impossible
7+