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.

Defining: 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?

  • 1
    $\begingroup$ What makes you think this is possible? i.e. if you have [1, 2, ...], what's the reversal of that? What's the "last" natural number that should be at the head of the list? $\endgroup$ Feb 15, 2019 at 21:22
  • $\begingroup$ @jmite, it is an exercise form my course work. However, I begin to think, that the intention of the exercise was to just flip the elements, not the whole stream. For example, binary elements such as Bools, then "True" elements would be "False" and vice versa. Given I can use "if else" expressions, this is easily doable. $\endgroup$
    – Imago
    Feb 16, 2019 at 10:04


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.