[Agda] Wish List

[Vag Vagoff]

* Allow main() to return arbitrary values and print them automatically 
on exit. (!!!)
>
> There is no convenient term representation around at runtime (values 
> are just Haskell values), so there's no way of printing arbitrary 
> values from compiled code. If you want that you can use the emacs mode 
> interpreter.
But it is possible to optionally insert prettyprinting call in Haskell's 
main code with all needed derivations performed.
>
> Can you do this with Unicode? Agda files are just UTF-8 encoded text 
> files which can be read as they are, and this is not going to change.
>  
AFAIK Unicode allows only predefined indices (0, 1, 2,...) but not 
arbitrary. May it be worth to devise a small utility to generate LaTeX 
sources from Agda declarations? It makes possible generation of sequents 
from data constructors too.

>
> Compiler or typechecker? There are known performance problems with the 
> typechecker, but I thought the compiler | was reasonably efficient.
>  
How to run typechecker without compiler?