97baef4 · Idris-dev · git.iko.soy

test/reg072/expecteddeleted−14

compare with master

unifiedsplit

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

122public export Mod.natexp can't refer to export Mod.natfn

123reg070.idr:7:1:

124Test_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 <<!

29:load reg068.idr

30:load reg069.idr

31:load reg070.idr

32+:load DoubleEquality.idr

32!

33!

33

34

34rm -f *.ibc

35rm -f *.ibc