[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