Consolidate reg018 into regression002
commit44fb18f1980b1544691171e09a29ae028bba444a
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:18 (10 years ago)
parent812566d
test/reg018/expecteddeleted−11
@@ -1,11 +0,0 @@
1−reg018a.idr:16:1:
2−conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
3−reg018a.idr:21:1:
4−conat.loopForever is possibly not total due to: conat.minusCoNat
5−reg018b.idr:8:1:
6−A.showB is possibly not total due to recursive path A.showB --> A.showB
7−reg018b.idr:11:1:
8−A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
9−reg018c.idr:21:1:
10−CodataTest.inf is possibly not total due to: with block in CodataTest.inf
11−reg018d.idr:8:1:Main.pull is not total as there are missing cases
test/reg018/rundeleted−6
@@ -1,6 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg018a.idr --check
3−${IDRIS:-idris} $@ reg018b.idr --check
4−${IDRIS:-idris} $@ reg018c.idr --check
5−${IDRIS:-idris} $@ reg018d.idr --check
6−rm *.ibc
test/regression002/expected+11
@@ -24,3 +24,14 @@ Specifically:
2424reg010.idr:5:15:
2525When checking left hand side of with block in usubst.unsafeSubst:
2626Can't match on with block in usubst.unsafeSubst warg a P x x px
27+reg018a.idr:16:1:
28+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
29+reg018a.idr:21:1:
30+conat.loopForever is possibly not total due to: conat.minusCoNat
31+reg018b.idr:8:1:
32+A.showB is possibly not total due to recursive path A.showB --> A.showB
33+reg018b.idr:11:1:
34+A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
35+reg018c.idr:21:1:
36+CodataTest.inf is possibly not total due to: with block in CodataTest.inf
37+reg018d.idr:8:1:Main.pull is not total as there are missing cases
test/reg018/reg018a.idr → test/regression002/reg018a.idrrenamed
The content is the same.
test/reg018/reg018b.idr → test/regression002/reg018b.idrrenamed
The content is the same.
test/reg018/reg018c.idr → test/regression002/reg018c.idrrenamed
The content is the same.
test/reg018/reg018d.idr → test/regression002/reg018d.idrrenamed
The content is the same.
test/regression002/run+4
@@ -6,6 +6,10 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
66:load reg006.idr
77:load reg007.lidr
88:load reg010.idr
9+:load reg018a.idr
10+:load reg018b.idr
11+:load reg018c.idr
12+:load reg018d.idr
913!
1014
1115rm -f *.ibc