ea745fc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Consolidate reg054 into regression002

commitea745fcfa0323cf18137d119bd0e1028f70dd1f5 authorSteven Shaw <steven@steshaw.org> dateFri 5 Aug 2016, 20:49 (10 years ago) parent88c66f9

5 files changed+14−15

compare with master

unifiedsplit

test/reg054/expected−13 test/reg054/run−2 test/regression002/expected+13 test/reg054/reg054.idr → test/regression002/reg054.idr test/regression002/run+1

test/reg054/expecteddeleted−13

@@ -1,13 +0,0 @@

1−reg054.idr:18:5:When checking left hand side of inf:

2−When checking an application of constructor Main.MkInfer:

3− Attempting concrete match on polymorphic argument: 0

4−reg054.idr:34:7:When checking left hand side of weird:

5−No explicit types on left hand side: Char

6−reg054.idr:37:8:When checking left hand side of weird':

7−No explicit types on left hand side: Nat

8−reg054.idr:40:1-8:When checking left hand side of tctrick:

9−When checking an application of Main.tctrick:

10− Type mismatch between

11− Maybe a1 (Type of Just x)

12− and

13− a (Expected type)

test/reg054/rundeleted−2

@@ -1,2 +0,0 @@

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg054.idr --check

test/regression002/expected+13

@@ -85,3 +85,16 @@ No such variable Bogus

8585 !!, expected: space

8686doubleBang mmn = do pure !!mmn

8787 ^

88+reg054.idr:18:5:When checking left hand side of inf:

89+When checking an application of constructor Main.MkInfer:

90+ Attempting concrete match on polymorphic argument: 0

91+reg054.idr:34:7:When checking left hand side of weird:

92+No explicit types on left hand side: Char

93+reg054.idr:37:8:When checking left hand side of weird':

94+No explicit types on left hand side: Nat

95+reg054.idr:40:1-8:When checking left hand side of tctrick:

96+When checking an application of Main.tctrick:

97+ Type mismatch between

98+ Maybe a1 (Type of Just x)

99+ and

100+ a (Expected type)

test/reg054/reg054.idr → test/regression002/reg054.idrrenamed

The content is the same.

test/regression002/run+1

@@ -22,6 +22,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!

2222:load working.idr

2323:load badbangop.idr

2424:load baddoublebang.idr

25+:load reg054.idr

2526!

2627

2728rm -f *.ibc