[Agda] Re: Lambda

[Lennart Augustsson]

Here's a pretty clean version of getting unicode reserved tokens.

On Wed, Jun 18, 2008 at 11:06 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:
>
>
> On Wed, Jun 18, 2008 at 6:56 PM, Lennart Augustsson <lennart at augustsson.net>
> wrote:
>>
>> Wow, using Unicode with Alex is massively ugly!
>> I thought making my suggested change would be trivial, but I was mistaken.
>
> Indeed. At the moment all unicode characters are replaced by a suitable
> ASCII dummy before showing a string to Alex. Adding the lambda would be
> quite easy I guess, just change the new lambda character to a backslash in
> the string that Alex sees. I'm not sure how to handle the arrow, though,
> since there you'd need to replace one character by two ASCII characters.
>
> I think the best way to do this is to just lex lambda and arrow as
> identifiers and let the parser sort things out.
>
> / Ulf
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: token.patch
Type: application/octet-stream
Size: 10078 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20080619/38019891/token-0001.obj