git.iko.soy/Idris-dev
on master help sign in
Fix output of unique001a
773ff9aEdwin Brady
test/unique001/expected+3−7
compare with master
unifiedsplit
@@ -2,19 +2,15 @@
219,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
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
438,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
6 Int -> String
6 Int -> String
7with
7with
8 UniqueType (Int -> String)
8 UniqueType (Int -> String)
9−unique001a.idr:49:12:Can't convert
9+unique001a.idr:44:12:Can't convert
10 Int -> String
10 Int -> String
11with
11with
12 UniqueType (Int -> String)
12 UniqueType (Int -> String)
13−unique001a.idr:60:12:Can't convert
13+unique001a.idr:55:12:Can't convert
14 UniqueType (Int -> String)
14 UniqueType (Int -> String)
15with
15with
16 Int -> String
16 Int -> String
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
19mkUList Z = []
19mkUList Z = []
20mkUList (S k) = cast k :: mkUList k
20mkUList (S k) = cast k :: mkUList k
21
21
22−-- showIt : UList Int -> Int -> String
23−-- showIt xs x = let xs' = umap (*2) xs in ""
24−
25showIt : UList Int -> Int -> String
22showIt : UList Int -> Int -> String
26−showIt [] y = "END"
23+showIt xs x = let xs' = umap (*2) xs in ""
27−showIt (x :: xs) y = let z = 0 :: xs in
28− show x ++ "," ++ showU xs ++ showU z
29
24
30printThings : (Int -> String) -> IO ()
25printThings : (Int -> String) -> IO ()
31printThings f = do putStrLn (f 10)
26printThings f = do putStrLn (f 10)