Test case that was accidentally accepted before
commit54451e462610b68474f00eb95b1b70d2c1335ae2
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateWed 11 Feb 2015, 17:50 (12 years ago)
parente0dc91e
test/totality006/expected+1
@@ -1,2 +1,3 @@
11totality006.idr:8:1:Main.prf is not total as there are missing cases
22totality006a.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 @@
11#!/usr/bin/env bash
22idris $@ totality006.idr --check
33idris $@ totality006a.idr --check
4+idris $@ totality006b.idr --check
45rm -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