@@ -14,13 +14,13 @@ import Prelude.List
15||| An infinite stream
15||| An infinite stream
16data Stream : Type -> Type where
16data Stream : Type -> Type where
17− (::) : (e : a) -> Inf (Stream a) -> Stream a
17+ (::) : (value : elem) -> Inf (Stream elem) -> Stream elem
19-- Hints for interactive editing
19-- Hints for interactive editing
20%name Stream xs,ys,zs,ws
20%name Stream xs,ys,zs,ws
22-- Usage hints for erasure analysis
22-- Usage hints for erasure analysis
23−%used Stream.(::) e
23+%used Stream.(::) value
25Functor Stream where
25Functor Stream where
26 map f (x::xs) = f x :: map f xs
26 map f (x::xs) = f x :: map f xs
@@ -42,7 +42,6 @@ take (S n) (x :: xs) = x :: (take n xs)
43||| Drop the first n elements from the stream
43||| Drop the first n elements from the stream
44||| @ n how many elements to drop
44||| @ n how many elements to drop
46drop : (n : Nat) -> Stream a -> Stream a
45drop : (n : Nat) -> Stream a -> Stream a
47drop Z xs = xs
46drop Z xs = xs
48drop (S k) (x::xs) = drop k xs
47drop (S k) (x::xs) = drop k xs