git.iko.soy/Idris-dev
on master help sign in
Test case that was accidentally accepted before
54451e4David Raymond Christiansen
test/totality006/expected+1
compare with master
unifiedsplit
@@ -1,2 +1,3 @@
1totality006.idr:8:1:Main.prf is not total as there are missing cases
1totality006.idr:8:1:Main.prf is not total as there are missing cases
2totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case
2totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case
3+totality006b.idr:10:1:totality006b.blargh is not total as there are missing cases
test/totality006/run+1
@@ -1,4 +1,5 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2idris $@ totality006.idr --check
2idris $@ totality006.idr --check
3idris $@ totality006a.idr --check
3idris $@ totality006a.idr --check
4+idris $@ totality006b.idr --check
4rm -f *.ibc
5rm -f *.ibc
test/totality006/totality006b.idrnew file+14
@@ -0,0 +1,14 @@
1+module totality006b
2+
3+import Data.So
4+
5+
6+-- There are approaches to impossibility checking that break on this
7+-- case but not on test006.idr, due to the extra computation.
8+total
9+blargh : (xs, ys : List a) -> So (length xs > length ys) -> GT (length xs) (length ys)
10+blargh [] [] Oh impossible
11+blargh [] (y :: xs) so = absurd so
12+blargh (y :: xs) [] Oh = LTESucc LTEZero
13+
14+-- Missing: blargh (y :: xs) (z :: ys) x = ?blargh_rhs_3