[Agda] Re: Agda FFI bindings

Alan Jeffrey ajeffrey at bell-labs.com
Tue Oct 5 03:22:35 CEST 2010


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.


More information about the Agda mailing list