[Agda] Wish List

[Ulf Norell]

On Tue, Sep 22, 2009 at 4:29 PM, Vag Vagoff <vag.vagoff at gmail.com> wrote:

>
> * 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.


> * Ability to make arbitrary indexes in variable names (as in <sub> <sub/>)
>

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.


> * 2.2.4 compiler is SO SLOW (even on my 1.8 GHZ dual core processor with
> 512 MB memory compilation takes more than 10 seconds)


Compiler or typechecker? There are known performance problems with the
typechecker, but I thought the compiler was reasonably efficient.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090922/45a7cdd8/attachment.html