[Agda] Wish List

[Ulf Norell]

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

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


lhs2TeX (http://people.cs.uu.nl/andres/lhs2tex/) can deal with Agda sources.



> 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?
>

>From the command line: agda Stuff.agda  (instead of agda --compile
Stuff.agda)
>From emacs: C-c C-l   (instead of C-c C-x C-c)

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