git.iko.soy/Idris-dev
on master help sign in
Consolidate reg068 into regression002
2e20173Steven Shaw
test/reg068/expecteddeleted−8
compare with master
unifiedsplit
@@ -1,8 +0,0 @@
1−reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
2−This is likely to lead to problems!
3−reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
4−This is likely to lead to problems!
5−reg068.idr:2:8-11:WARNING: nat is bound as an implicit
6− Did you mean to refer to Main.nat?
7−reg068.idr:2:6:When checking constructor Main.ze:
8−Type level variable nat is not Main.nat
test/reg068/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg068.idr --check
3−rm -f *.ibc
test/regression002/expected+9
@@ -109,3 +109,12 @@ reg055a.idr:13:7:When checking left hand side of Foo.apply:
109Can't match on apply (\x => \y => x) a
109Can't match on apply (\x => \y => x) a
110reg056.idr:7:7:dodgy n m Refl is a valid case
110reg056.idr:7:7:dodgy n m Refl is a valid case
111reg056.idr:10:6:nonk Refl is a valid case
111reg056.idr:10:6:nonk Refl is a valid case
112+reg068.idr:1:6:
113+Main.nat has a name which may be implicitly bound.
114+This is likely to lead to problems!
115+reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
116+This is likely to lead to problems!
117+reg068.idr:2:8-11:WARNING: nat is bound as an implicit
118+ Did you mean to refer to Main.nat?
119+reg068.idr:2:6:When checking constructor Main.ze:
120+Type level variable nat is not Main.nat
test/reg068/reg068.idr → test/regression002/reg068.idrrenamed

The content is the same.

test/regression002/run+1
@@ -26,6 +26,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
26:load reg055.idr
26:load reg055.idr
27:load reg055a.idr
27:load reg055a.idr
28:load reg056.idr
28:load reg056.idr
29+:load reg068.idr
29!
30!
30
31
31rm -f *.ibc
32rm -f *.ibc