git.iko.soy/Idris-dev
on master help sign in
Consolidate reg018 into regression002
44fb18fSteven Shaw
test/reg018/expecteddeleted−11
compare with master
unifiedsplit
@@ -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:
24reg010.idr:5:15:
24reg010.idr:5:15:
25When checking left hand side of with block in usubst.unsafeSubst:
25When checking left hand side of with block in usubst.unsafeSubst:
26Can't match on with block in usubst.unsafeSubst warg a P x x px
26Can'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 <<!
6:load reg006.idr
6:load reg006.idr
7:load reg007.lidr
7:load reg007.lidr
8:load reg010.idr
8:load reg010.idr
9+:load reg018a.idr
10+:load reg018b.idr
11+:load reg018c.idr
12+:load reg018d.idr
9!
13!
10
14
11rm -f *.ibc
15rm -f *.ibc