On 2010-10-04 22:57, Alan Jeffrey wrote:
> Yes, that I get, I just don't understand why not just include a
> postulate inf : forall {A} -> \inf(IO A) -> (IO A), and get rid of the
> distinction between IO.Primitive.IO and IO.IO.
Because Agda uses guarded corecursion, and postulates are not treated as
constructors.
--
/NAD