git.iko.soy/Idris-dev
on master help sign in
Consolidate reg068 into regression002
commit2e20173597773a9e77e711a96bb3f37ea790918a authorSteven Shaw <steven@steshaw.org> dateFri 5 Aug 2016, 20:54 (10 years ago) parente2f1da2
5 files changed+10−11
compare with master
unifiedsplit
test/reg068/expected−8 test/reg068/run−3 test/regression002/expected+9 test/reg068/reg068.idr → test/regression002/reg068.idr test/regression002/run+1
test/reg068/expecteddeleted−8
@@ -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:
109109Can't match on apply (\x => \y => x) a
110110reg056.idr:7:7:dodgy n m Refl is a valid case
111111reg056.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 <<!
2626:load reg055.idr
2727:load reg055a.idr
2828:load reg056.idr
29+:load reg068.idr
2930!
3031
3132rm -f *.ibc