@@ -7,6 +7,29 @@ codata CoList : Type -> Type where
77 Nil : CoList a
88 (::) : a -> CoList a -> CoList a
99
10+infixr 7 ++
11+
12+||| Append two CoLists
13+(++) : CoList a -> CoList a -> CoList a
14+(++) [] right = right
15+(++) (x::xs) right = x :: (xs ++ right)
16+
17+instance Semigroup (CoList a) where
18+ (<+>) = (++)
19+
20+instance Monoid (CoList a) where
21+ neutral = []
22+
23+instance Functor CoList where
24+ map f [] = []
25+ map f (x::xs) = f x :: map f xs
26+
27+instance Show a => Show (CoList a) where
28+ show xs = "[" ++ show' "" xs ++ "]" where
29+ show' acc [] = acc
30+ show' acc [x] = acc ++ show x
31+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
32+
1033||| Take the first `n` elements of `xs`
1134|||
1235||| If there are not enough elements, return the whole coList.