c2113d7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Consolidate unique002 into unique004

c2113d7Steven Shaw10 years ago

test/unique002/expecteddeleted−5

@@ -1,5 +0,0 @@

1−unique002.idr:15:5:Unique name xs is used more than once

2−unique002a.idr:15:5:Type mismatch between

3− Int -> String

4−and

5− UniqueType (Int -> String)

test/unique002/rundeleted−4

@@ -1,4 +0,0 @@

1−#!/usr/bin/env bash

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

3−${IDRIS:-idris} $@ --nocolour unique002a.idr --check

4−rm -f *.ibc

test/unique004/expected+5

@@ -15,3 +15,8 @@ unique001c.idr:46:6:Unique name f is used more than once

15unique001d.idr:3:7:Borrowed name x must not be used on RHS

16unique001e.idr:3:10:

17Constructor Main.Nil has a UniqueType, but the data type does not

18+unique002.idr:15:5:Unique name xs is used more than once

19+unique002a.idr:15:5:Type mismatch between

20+ Int -> String

21+and

22+ UniqueType (Int -> String)

test/unique004/run+2

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

6:load unique001c.idr

7:load unique001d.idr

8:load unique001e.idr

9+:load unique002.idr

10+:load unique002a.idr

11!

11rm -f *.ibc

13rm -f *.ibc

test/unique002/unique002.idr → test/unique004/unique002.idrrenamed

The content is the same.

test/unique002/unique002a.idr → test/unique004/unique002a.idrrenamed

The content is the same.