[Agda] Superscript l and r in unicode

[Dr. ÉRDI Gergő]

You should get a menu of possible Unicode characters in the minibuf when
you type \^l, and you can choose from them with cursor keys. The selection
is "sticky" in that the next insert with default to the last selection.

On Feb 9, 2018 13:44, "Philip Wadler" <wadler at inf.ed.ac.uk> wrote:

The documentation says that one should type

  \^l

to get a superscript l in unicode, and similarly for superscript r.

However, the documentation also says that one should type the exact same
sequence

  \^l

to get a leftward pointing superscript arrow, and similarly with r for a
rightward pointing arrow.

In my emacs, the latter wins out. How do I get a superscript l or r letter?

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180209/69f71f69/attachment.html>