test/unique001/expected · Idris-dev

git.iko.soy/Idris-dev

on 7afa310 help sign in

20 lines 887 B history raw

119,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

219,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5unique001a.idr:33:11:Can't convert

6 [94mInt[0m -> [94mString[0m

7with

8 UniqueType ([94mInt[0m -> [94mString[0m)

9unique001a.idr:44:12:Can't convert

10 [94mInt[0m -> [94mString[0m

11with

12 UniqueType ([94mInt[0m -> [94mString[0m)

13unique001a.idr:55:12:Can't convert

14 UniqueType ([94mInt[0m -> [94mString[0m)

15with

16 [94mInt[0m -> [94mString[0m

17unique001b.idr:16:7:Borrowed name xs must not be used on RHS

18unique001c.idr:49:6:Unique name f is used more than once

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

20unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not