@@ -90,13 +90,6 @@ unzip3 xs = (map (\(x,_,_) => x) xs, map (\(_,x,_) => x) xs, map (\(_,_,x) => x)
9090diag : Stream (Stream a) -> Stream a
9191diag ((x::xs)::xss) = x :: diag (map tail xss)
9292
93−||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.
94−||| @ f the combining function
95−||| @ xs the Stream to fold up
96−partial -- the recursive call isn't guarded!
97−foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b
98−foldr f (x :: xs) = f x (foldr f xs)
99−
10093||| Produce a Stream of left folds of prefixes of the given Stream
10194||| @ f the combining function
10295||| @ acc the initial value
@@ -104,14 +97,6 @@ foldr f (x :: xs) = f x (foldr f xs)
10497scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
10598scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
10699
107−||| Produce a Stream of (corecursive) right folds of tails of the given Stream
108−||| @ f the combining function
109−||| @ xs the Stream to fold up
110−-- Reusing the head of the corecursion in the obvious way doesn't productivity check
111−partial -- and the call to foldr isn't guarded anyway!
112−scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
113−scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
114−
115100||| Produce a Stream repeating a sequence
116101||| @ xs the sequence to repeat
117102||| @ ok proof that the list is non-empty