Following is the definition of codata stream:
codata Stream where hd : Stream −> A tl : Stream −> Stream
For simplicity I assume I have just a binary stream. Now I would like to define a function
flip : Stream -> Stream , that reverses the order of the stream elements.
hd(flip S) = head (S) is pretty simple.
However I don't see how one can define
tl(flip S)) properly. Does anyone have an idea, if this is possible and if yes, how?