At any rate, if you intend to prove this for any arbitrary f, I
can't
tell you how to prove it formally because it's not true.
How do you know that? Can you give an example where it fails?
The problem with the code you originally posted was that it looked
like this:
f r = do r' <- something
f r'
something else -- this is dead code
That is, the computation is non-terminating, because f simply calls
itself recursively, with no base case.
Regards,
Malcolm
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
