773ff9a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix output of unique001a

commit773ff9a8256906bc0b6e97b55843b15617d3aef0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Aug 2014, 20:34 (12 years ago) parentc55895d

2 files changed+4−13

unifiedsplit

test/unique001/expected+3−7

@@ -2,19 +2,15 @@

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

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

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

5−unique001a.idr:38:11:Can't convert

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

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

77with

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

9−unique001a.idr:49:12:Can't convert

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

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

1111with

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

13−unique001a.idr:60:12:Can't convert

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

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

1515with

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

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

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

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

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

test/unique001/unique001a.idr+1−6

@@ -19,13 +19,8 @@ mkUList : Nat -> UList Int

1919mkUList Z = []

2020mkUList (S k) = cast k :: mkUList k

2121

22−-- showIt : UList Int -> Int -> String

23−-- showIt xs x = let xs' = umap (*2) xs in ""

24−

2522showIt : UList Int -> Int -> String

26−showIt [] y = "END"

27−showIt (x :: xs) y = let z = 0 :: xs in

28− show x ++ "," ++ showU xs ++ showU z

23+showIt xs x = let xs' = umap (*2) xs in ""

2924

3025printThings : (Int -> String) -> IO ()

3126printThings f = do putStrLn (f 10)