[Agda] Superscript l and r in unicode

[N. Raghavendra]

At 2018-02-08T17:36:13-04:00, Philip Wadler 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?

In my installation of `agda-input', when I type "\^l", the minibuffer
window shows the choices "1.⃖ 2.⃐ 3.⃔ 4.ˡ"; to choose "ˡ", I now type "4",
and to choose "⃖", I now type "1".  Moreover, the package makes the last
choice the current default.  Thus, after I type "⃔" with "\^l3", then
"\^l[SPC]" inserts "⃔" into the buffer.

Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/