eac558e · Idris-dev · git.iko.soy

test/reg023/expecteddeleted−7

@@ -1,7 +0,0 @@

1−reg023.idr:7:5:When checking right hand side of bad with expected type

2− f Nat

3−

4−Type mismatch between

5− Nat (Type of 0)

6−and

7− f Nat (Expected type)

test/reg023/rundeleted−3

@@ -1,3 +0,0 @@

1−#!/usr/bin/env bash

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

3−rm -f *.ibc

test/regression002/expected+7

@@ -35,3 +35,10 @@ A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

35reg018c.idr:21:1:

36CodataTest.inf is possibly not total due to: with block in CodataTest.inf

37reg018d.idr:8:1:Main.pull is not total as there are missing cases

38+reg023.idr:7:5:When checking right hand side of bad with expected type

39+ f Nat

40+

41+Type mismatch between

42+ Nat (Type of 0)

43+and

44+ f Nat (Expected type)

test/reg023/reg023.idr → test/regression002/reg023.idrrenamed

The content is the same.

test/regression002/run+1

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

10:load reg018b.idr

11:load reg018c.idr

12:load reg018d.idr

13+:load reg023.idr

13!

14!

14

15

15rm -f *.ibc

16rm -f *.ibc