2bf2038 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Consolidate reg055 into regression002

2bf2038Steven Shaw10 years ago

test/reg055/expecteddeleted−9

compare with master

unifiedsplit

@@ -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:

98 Maybe a1 (Type of Just x)

99 and

100 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 <<!

23:load badbangop.idr

24:load baddoublebang.idr

25:load reg054.idr

26+:load reg055.idr

27+:load reg055a.idr

26!

28!

28rm -f *.ibc

30rm -f *.ibc