@@ -1,6 +1,7 @@
1module Data.CoList
1module Data.CoList
3%access public
3%access public
5||| Idris will know that it always can produce a new element in finite time
6||| Idris will know that it always can produce a new element in finite time
6codata CoList : Type -> Type where
7codata CoList : Type -> Type where
@@ -23,10 +24,14 @@ instance Functor CoList where
23 map f (x::xs) = f x :: map f xs
24 map f (x::xs) = f x :: map f xs
25instance Show a => Show (CoList a) where
26instance Show a => Show (CoList a) where
26− show xs = "[" ++ show' "" xs ++ "]" where
27+ show xs = "[" ++ show' "" 20 xs ++ "]" where
28+ show' : String -> (n : Nat) -> (xs : CoList a) -> String
27− show' acc [] = acc
30+ show' acc (S n) [] = acc
28− show' acc [x] = acc ++ show x
31+ show' acc (S n) [x] = acc ++ show x
32+ show' acc (S n) (x :: xs) =
29− show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
33+ if n > 0 then show' (acc ++ (show x) ++ ", ") n xs
34+ else acc ++ (show x) ++ "..."
31||| Take the first `n` elements of `xs`
36||| Take the first `n` elements of `xs`