[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

On 10/04/2010 05:10 PM, Nils Anders Danielsson wrote:
> 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.

Urg.  Good point.  Using a coninductive datatype with a run function 
allows the --no-termination-check option to be local to the IO module, 
whereas there's no similar "honest I'm a constructor" option.

A.