agda2scheme
agda2scheme copied to clipboard
jespercockx
Compiler backend for generating Scheme code
In order to support custom primitives for doing IO and such, it would be good to support `FOREIGN` pragmas to include snippets of Scheme code into the Agda source.
In order to make the backend practically useable, it needs to have support for imports from other files. One choice that needs to be made is whether we compile each...
Currently Agda2Scheme compiles Agda definitions to Scheme definitions, but there is no way yet to indicate a main function. One question here is whether we want something like the IO...