[Agda] reflection via FFI?

[Ulf Norell]

No, there's no way to do this. I'm not aware of any stable way of
dynamically compiling and running Haskell code.

/ Ulf

On Fri, Oct 14, 2016 at 1:02 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> Is there a way to do this? I'd like to write something like foo :: Term ->
> TC Term (in Haskell) and invoke it from Agda such that Agda "knows" what
> gets returned (in the same way that it knows the values of other builtin
> reflection functions). I don't think this is possible at the moment:
> afaics, the FFI only allows Agda to "call out", leaving the results of the
> call obscured behind a postulate.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161014/017205d5/attachment.html