[Agda] Simple Agda Libraries

[Lennart Augustsson]

I found the TeX input method an excellent (if somewhat slow) way to
enter Unicode when writing Agda.

  -- Lennart

On Mon, Jan 12, 2009 at 8:35 AM, James McKinna <james at fixedpoint.org> wrote:
> Thanks Wouter for this (admittedly retrograde) step.
>
> As a very old-fashioned person, I nevertheless love the mixfixes in Agda,
> while loathing the Unicode, because ... I just have not learned to upgrade
> my typing style/my mental model of what keystrokes turn into what glyphs
> (and I am getting a bit old to learn a set of character tables/ \uxxxx
> escapes by rote, I reckon).
>
> I know this isn't just old-fashionedness, but the ingrained Anglo cultural
> bias which ASCII and ASCII keyboards have left us with, and which it would
> be good to outgrow (I guess everyone else had previously to learn a lot of
> escape sequences and tables for Chinese and Japanese, bvb.).
>
> As well as supporting Wouter's idea, could the Unicode experts offer some
> insight into how to migrate to using it effectively?
>
> Apologies for the naivete of the question, but it is meant seriously.
>
> James
>
> Wouter Swierstra wrote:
>>
>> Dear all,
>>
>> I have to admit I'm a bit hesitant to use the standard libraries. It has a
>> bit too much Unicode mixfix madness for my taste. Call me old-fashioned, but
>> I quite like identifiers everyone immediately knows how to type.
>> ...
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>