@@ -7,6 +7,29 @@ codata CoList : Type -> Type where
7 Nil : CoList a
7 Nil : CoList a
8 (::) : a -> CoList a -> CoList a
8 (::) : a -> CoList a -> CoList a
12+||| Append two CoLists
13+(++) : CoList a -> CoList a -> CoList a
15+(++) (x::xs) right = x :: (xs ++ right)
17+instance Semigroup (CoList a) where
20+instance Monoid (CoList a) where
23+instance Functor CoList where
25+ map f (x::xs) = f x :: map f xs
27+instance Show a => Show (CoList a) where
28+ show xs = "[" ++ show' "" xs ++ "]" where
30+ show' acc [x] = acc ++ show x
31+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
10||| Take the first `n` elements of `xs`
33||| Take the first `n` elements of `xs`
12||| If there are not enough elements, return the whole coList.
35||| If there are not enough elements, return the whole coList.