[Agda] reflection via FFI?

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


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.


More information about the Agda mailing list