git.iko.soy/Idris-dev
on master help sign in
Consolidate reg072 into regression002
commit97baef406d42f8fcd52a06e87c0f4cdf4e3ad27c authorSteven Shaw <steven@steshaw.org> dateFri 5 Aug 2016, 20:59 (10 years ago) parent5208aeb
5 files changed+16−17
compare with master
unifiedsplit
test/reg072/expected−14 test/reg072/run−3 test/reg072/DoubleEquality.idr → test/regression002/DoubleEquality.idr test/regression002/expected+15 test/regression002/run+1
test/reg072/expecteddeleted−14
@@ -1,14 +0,0 @@
1−DoubleEquality.idr:4:87:When checking right hand side of oops with expected type
2− Void
3−
4−When checking argument value to function Prelude.Basics.the:
5− Type mismatch between
6− x = x (Type of Refl)
7− and
8− (-0.0) = 0.0 (Expected type)
9−
10− Specifically:
11− Type mismatch between
12− -0.0
13− and
14− 0.0
test/reg072/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ DoubleEquality.idr --check
3−rm -f *.ibc
test/reg072/DoubleEquality.idr → test/regression002/DoubleEquality.idrrenamed

The content is the same.

test/regression002/expected+15
@@ -122,3 +122,18 @@ Mod.idr:11:1:
122122public export Mod.natexp can't refer to export Mod.natfn
123123reg070.idr:7:1:
124124Test_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
125+DoubleEquality.idr:4:87:
126+When checking right hand side of oops with expected type
127+ Void
128+
129+When checking argument value to function Prelude.Basics.the:
130+ Type mismatch between
131+ x = x (Type of Refl)
132+ and
133+ (-0.0) = 0.0 (Expected type)
134+
135+ Specifically:
136+ Type mismatch between
137+ -0.0
138+ and
139+ 0.0
test/regression002/run+1
@@ -29,6 +29,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
2929:load reg068.idr
3030:load reg069.idr
3131:load reg070.idr
32+:load DoubleEquality.idr
3233!
3334
3435rm -f *.ibc