Consolidate unique002 into unique004
commitc2113d706f4cccfaaf13adfe6ec369be2de85646
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 22:33 (10 years ago)
parent006b884
test/unique002/expecteddeleted−5
@@ -1,5 +0,0 @@
1−unique002.idr:15:5:Unique name xs is used more than once
2−unique002a.idr:15:5:Type mismatch between
3− Int -> String
4−and
5− UniqueType (Int -> String)
test/unique002/rundeleted−4
@@ -1,4 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour unique002.idr --check
3−${IDRIS:-idris} $@ --nocolour unique002a.idr --check
4−rm -f *.ibc
test/unique004/expected+5
@@ -15,3 +15,8 @@ unique001c.idr:46:6:Unique name f is used more than once
1515unique001d.idr:3:7:Borrowed name x must not be used on RHS
1616unique001e.idr:3:10:
1717Constructor Main.Nil has a UniqueType, but the data type does not
18+unique002.idr:15:5:Unique name xs is used more than once
19+unique002a.idr:15:5:Type mismatch between
20+ Int -> String
21+and
22+ UniqueType (Int -> String)
test/unique004/run+2
@@ -6,6 +6,8 @@ ${IDRIS:-idris} --nobanner --nocolour --quiet <<!
66:load unique001c.idr
77:load unique001d.idr
88:load unique001e.idr
9+:load unique002.idr
10+:load unique002a.idr
911!
1012
1113rm -f *.ibc
test/unique002/unique002.idr → test/unique004/unique002.idrrenamed
The content is the same.
test/unique002/unique002a.idr → test/unique004/unique002a.idrrenamed
The content is the same.