[Agda] Simple Agda Libraries

Marcin Benke ben at mimuw.edu.pl
Mon Jan 12 11:11:45 CET 2009


2009/1/12 James McKinna <james at fixedpoint.org>:
> 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).

While I can understand your attitude to the "Unicode madness", let me
remind you (and other readers of the Agda list) of the TeX input
method. Enable it and you can type in Unicode whatever (well, most of)
what you can type in TeX.

Nonetheless, kudos to Wouter for his idea and work.

-- 
Marcin Benke


More information about the Agda mailing list