git.iko.soy/Idris-dev
on master help sign in
Consolidate reg007 into regression002
7701a90Steven Shaw
test/reg007/A.lidr → test/regression002/A.lidrrenamed
compare with master
unifiedsplit

The content is the same.

test/regression002/expected+15
@@ -6,3 +6,18 @@ reg003a.idr:9:6:When checking type of Main.test:
6No such variable EvenList
6No such variable EvenList
7reg006.idr:17:1:
7reg006.idr:17:1:
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
9+reg007.lidr:8:1:A.n is already defined
10+reg007.lidr:12:11-17:
11+When checking right hand side of hurrah with expected type
12+ 0 = 1
13+
14+Type mismatch between
15+ n = lala (Type of isSame)
16+and
17+ 0 = 1 (Expected type)
18+
19+Specifically:
20+ Type mismatch between
21+ 1
22+ and
23+ 0
test/reg007/reg007.lidr → test/regression002/reg007.lidrrenamed

The content is the same.

test/regression002/run+1
@@ -4,6 +4,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
4:load reg003.idr
4:load reg003.idr
5:load reg003a.idr
5:load reg003a.idr
6:load reg006.idr
6:load reg006.idr
7+:load reg007.lidr
7!
8!
8
9
9rm -f *.ibc
10rm -f *.ibc