4a23805 · Idris-dev · git.iko.soy

test/basic010/run+2−2

@@ -4,7 +4,7 @@ set -eu

4

5TIMEOUT=../scripts/timeout

6

7−$TIMEOUT 10 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010

7+$TIMEOUT 20 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010

8−$TIMEOUT 5 ./basic010

8+$TIMEOUT 20 ./basic010

9

10rm -f -- *.ibc basic010

test/regression002/expected+2−2

@@ -6,8 +6,8 @@ reg003a.idr:9:6:When checking type of Main.test:

6No such variable EvenList

7reg006.idr:17:1:

8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

9−reg007.lidr:8:1:A.n is already defined

9+reg007.lidr:8:3:A.n is already defined

10−reg007.lidr:12:11-17:When checking right hand side of hurrah with expected type

10+reg007.lidr:12:13-19:When checking right hand side of hurrah with expected type

11 0 = 1

12

13Type mismatch between

test/totality011/expected+1−1

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

1−totality011.lidr:22:1:

1+totality011.lidr:22:3:

2Main.weCanOnlyGetOlder is not total as there are missing cases