[Agda] reflection via FFI?

[Ulf Norell]

What's your use case? Agda IO is implemented using the FFI so calling
arbitrary IO functions from TC is not possible. Internally TC runs on top
of IO though, so if you have a particular IO function in mind it could
conceivably be added as a primitive.

/ Ulf

On Fri, Oct 14, 2016 at 9:54 AM, Roman <effectfully at gmail.com> wrote:

> Sorry for the off-topic, but is it possible to run a TC computation
> inside the IO monad? Would be nice to type check terms that come from
> IO in IO.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161014/862670da/attachment.html