@@ -14,13 +14,13 @@ import Prelude.List
1414
1515||| An infinite stream
1616data Stream : Type -> Type where
17− (::) : (e : a) -> Inf (Stream a) -> Stream a
17+ (::) : (value : elem) -> Inf (Stream elem) -> Stream elem
1818
1919-- Hints for interactive editing
2020%name Stream xs,ys,zs,ws
2121
2222-- Usage hints for erasure analysis
23−%used Stream.(::) e
23+%used Stream.(::) value
2424
2525Functor Stream where
2626 map f (x::xs) = f x :: map f xs
@@ -42,7 +42,6 @@ take (S n) (x :: xs) = x :: (take n xs)
4242
4343||| Drop the first n elements from the stream
4444||| @ n how many elements to drop
45−%assert_total
4645drop : (n : Nat) -> Stream a -> Stream a
4746drop Z xs = xs
4847drop (S k) (x::xs) = drop k xs