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$ – jmite Feb 15 '19 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 '19 at 10:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.