Consolidate reg055 into regression002
commit2bf203888e509557265469fb82c1ff739f80bb2f
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:50 (10 years ago)
parentea745fc
test/reg055/expecteddeleted−9
@@ -1,9 +0,0 @@
1−reg055.idr:5:3:When checking left hand side of g:
2−Can't match on g (f 0)
3−reg055.idr:8:3:When checking left hand side of h:
4−Can't match on h x x
5−reg055a.idr:8:5:When checking left hand side of foo:
6−When checking an application of constructor Foo.CAny:
7− Attempting concrete match on polymorphic argument: Nothing
8−reg055a.idr:13:7:When checking left hand side of Foo.apply:
9−Can't match on apply (\x => \y => x) a
test/reg055/rundeleted−5
@@ -1,5 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour reg055.idr --check
3−${IDRIS:-idris} $@ --nocolour reg055a.idr --check
4−rm -f *.ibc
5−
test/regression002/expected+9
@@ -98,3 +98,12 @@ When checking an application of Main.tctrick:
9898 Maybe a1 (Type of Just x)
9999 and
100100 a (Expected type)
101+reg055.idr:5:3:When checking left hand side of g:
102+Can't match on g (f 0)
103+reg055.idr:8:3:When checking left hand side of h:
104+Can't match on h x x
105+reg055a.idr:8:5:When checking left hand side of foo:
106+When checking an application of constructor Foo.CAny:
107+ Attempting concrete match on polymorphic argument: Nothing
108+reg055a.idr:13:7:When checking left hand side of Foo.apply:
109+Can't match on apply (\x => \y => x) a
test/reg055/reg055.idr → test/regression002/reg055.idrrenamed
The content is the same.
test/reg055/reg055a.idr → test/regression002/reg055a.idrrenamed
The content is the same.
test/regression002/run+2
@@ -23,6 +23,8 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
2323:load badbangop.idr
2424:load baddoublebang.idr
2525:load reg054.idr
26+:load reg055.idr
27+:load reg055a.idr
2628!
2729
2830rm -f *.ibc