[Agda] reflection via FFI?

[Ulf Norell]

On Fri, Oct 14, 2016 at 2:24 PM, Roman <effectfully at gmail.com> wrote:

> Sorry, I wasn't clear enough. I mean the other way around: `runTC : ∀
> {α} {A : Set α} -> TC A -> IO A`. I want to type check some runtime
> terms using TC facilities.
>

You would have to call the Agda Haskell library through FFI for that. We
don't
include the Agda implementation in compiled Agda programs.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161014/3f96335b/attachment.html