@@ -1,6 +1,7 @@
11module Data.CoList
22
33%access public
4+-- %default total
45
56||| Idris will know that it always can produce a new element in finite time
67codata CoList : Type -> Type where
@@ -23,10 +24,14 @@ instance Functor CoList where
2324 map f (x::xs) = f x :: map f xs
2425
2526instance Show a => Show (CoList a) where
26− show xs = "[" ++ show' "" xs ++ "]" where
27− show' acc [] = acc
28− show' acc [x] = acc ++ show x
29− show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
27+ show xs = "[" ++ show' "" 20 xs ++ "]" where
28+ show' : String -> (n : Nat) -> (xs : CoList a) -> String
29+ show' acc Z _ = acc
30+ show' acc (S n) [] = acc
31+ show' acc (S n) [x] = acc ++ show x
32+ show' acc (S n) (x :: xs) =
33+ if n > 0 then show' (acc ++ (show x) ++ ", ") n xs
34+ else acc ++ (show x) ++ "..."
3035
3136||| Take the first `n` elements of `xs`
3237|||