git.iko.soy/Idris-dev
on master help sign in
Fold tests into regression002.
commitea0f628be46cd6d0b67b752471f0bc4bf25eae41 authorBjörn Aili <bjorn.aili@gmail.com> dateSun 7 Aug 2016, 17:52 (10 years ago) parent635fb40
8 files changed+16−20
compare with master
unifiedsplit
test/reg076/expected−8 test/reg076/run−3 test/reg077/expected−6 test/reg077/run−3 test/regression002/expected+14 test/reg076/reg076.idr → test/regression002/reg076.idr test/reg077/reg077.idr → test/regression002/reg077.idr test/regression002/run+2
test/reg076/expecteddeleted−8
@@ -1,8 +0,0 @@
1−./reg076.idr:8:1: error: Missing
2− fixity declaration for
3− Main.:>, expected: "->", "=>",
4− ambiguous use of a left-associative operator,
5− ambiguous use of a non-associative operator,
6− ambiguous use of a right-associative operator
7−<EOF>
8−^
test/reg076/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg076.idr --check
3−rm -f *.ibc
test/reg077/expecteddeleted−6
@@ -1,6 +0,0 @@
1−./reg077.idr:3:1: error: Missing
2− fixity declaration for
3− Main.:>>, expected: ")", ";",
4− "in", start of block
5−<EOF>
6−^
test/reg077/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg077.idr --check
3−rm -f *.ibc
test/regression002/expected+14
@@ -117,6 +117,20 @@ Type level variable nat is not Main.nat
117117Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn
118118reg070.idr:7:1:
119119Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
120+./reg076.idr:8:1: error: Missing
121+ fixity declaration for
122+ Main.:>, expected: "->", "=>",
123+ ambiguous use of a left-associative operator,
124+ ambiguous use of a non-associative operator,
125+ ambiguous use of a right-associative operator
126+<EOF>
127+^
128+./reg077.idr:3:1: error: Missing
129+ fixity declaration for
130+ Main.:>>, expected: ")", ";",
131+ "in", start of block
132+<EOF>
133+^
120134DoubleEquality.idr:4:87:When checking right hand side of oops with expected type
121135 Void
122136
test/reg076/reg076.idr → test/regression002/reg076.idrrenamed

The content is the same.

test/reg077/reg077.idr → test/regression002/reg077.idrrenamed

The content is the same.

test/regression002/run+2
@@ -29,6 +29,8 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
2929:load reg068.idr
3030:load reg069.idr
3131:load reg070.idr
32+:load reg076.idr
33+:load reg077.idr
3234:load DoubleEquality.idr
3335!
3436