Consolidate reg023 into regression002
commiteac558e6ea5a7d829a816baf537fcf7856281237
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:27 (10 years ago)
parent44fb18f
test/reg023/expecteddeleted−7
@@ -1,7 +0,0 @@
1−reg023.idr:7:5:When checking right hand side of bad with expected type
2− f Nat
3−
4−Type mismatch between
5− Nat (Type of 0)
6−and
7− f Nat (Expected type)
test/reg023/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour reg023.idr --check
3−rm -f *.ibc
test/regression002/expected+7
@@ -35,3 +35,10 @@ A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
3535reg018c.idr:21:1:
3636CodataTest.inf is possibly not total due to: with block in CodataTest.inf
3737reg018d.idr:8:1:Main.pull is not total as there are missing cases
38+reg023.idr:7:5:When checking right hand side of bad with expected type
39+ f Nat
40+
41+Type mismatch between
42+ Nat (Type of 0)
43+and
44+ f Nat (Expected type)
test/reg023/reg023.idr → test/regression002/reg023.idrrenamed
The content is the same.
test/regression002/run+1
@@ -10,6 +10,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
1010:load reg018b.idr
1111:load reg018c.idr
1212:load reg018d.idr
13+:load reg023.idr
1314!
1415
1516rm -f *.ibc