@@ -26,12 +26,10 @@ instance Functor CoList where
26instance Show a => Show (CoList a) where
26instance Show a => Show (CoList a) where
27 show xs = "[" ++ show' "" 20 xs ++ "]" where
27 show xs = "[" ++ show' "" 20 xs ++ "]" where
28 show' : String -> (n : Nat) -> (xs : CoList a) -> String
28 show' : String -> (n : Nat) -> (xs : CoList a) -> String
29− show' acc Z _ = acc
29+ show' acc Z _ = acc ++ "..."
30 show' acc (S n) [] = acc
30 show' acc (S n) [] = acc
31 show' acc (S n) [x] = acc ++ show x
31 show' acc (S n) [x] = acc ++ show x
32− show' acc (S n) (x :: xs) =
32+ show' acc (S n) (x :: xs) = show' (acc ++ (show x) ++ ", ") n xs
33− if n > 0 then show' (acc ++ (show x) ++ ", ") n xs
34− else acc ++ (show x) ++ ", ..."
36||| Take the first `n` elements of `xs`
34||| Take the first `n` elements of `xs`