@@ -90,13 +90,6 @@ unzip3 xs = (map (\(x,_,_) => x) xs, map (\(_,x,_) => x) xs, map (\(_,_,x) => x)
90diag : Stream (Stream a) -> Stream a
90diag : Stream (Stream a) -> Stream a
91diag ((x::xs)::xss) = x :: diag (map tail xss)
91diag ((x::xs)::xss) = x :: diag (map tail xss)
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)
100||| Produce a Stream of left folds of prefixes of the given Stream
93||| Produce a Stream of left folds of prefixes of the given Stream
101||| @ f the combining function
94||| @ f the combining function
102||| @ acc the initial value
95||| @ acc the initial value
@@ -104,14 +97,6 @@ foldr f (x :: xs) = f x (foldr f xs)
104scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
97scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Stream b) -> Stream a
105scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
98scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
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
115||| Produce a Stream repeating a sequence
100||| Produce a Stream repeating a sequence
116||| @ xs the sequence to repeat
101||| @ xs the sequence to repeat
117||| @ ok proof that the list is non-empty
102||| @ ok proof that the list is non-empty