[Agda] reflection via FFI?

Roman effectfully at gmail.com
Fri Oct 14 14:24:45 CEST 2016


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.


More information about the Agda mailing list