<div dir="ltr">Thank you to Gergő Érdi and N. Raghavendra for helping with my newbie question. I had seen only the options for leftward arrows after typing \^l, and failed to spot that superscript l was the final option. Cheers, -- P<br></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 10 February 2018 at 02:59, N. Raghavendra <span dir="ltr"><<a href="mailto:nyraghu27132@gmail.com" target="_blank">nyraghu27132@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">At 2018-02-08T17:36:13-04:00, Philip Wadler wrote:<br>
<br>
> The documentation says that one should type<br>
><br>
>   \^l<br>
><br>
> to get a superscript l in unicode, and similarly for superscript r.<br>
><br>
> However, the documentation also says that one should type the exact<br>
> same sequence<br>
><br>
>   \^l<br>
><br>
> to get a leftward pointing superscript arrow, and similarly with r<br>
> for a rightward pointing arrow.<br>
><br>
> In my emacs, the latter wins out. How do I get a superscript l or r<br>
> letter?<br>
<br>
</span>In my installation of `agda-input', when I type "\^l", the minibuffer<br>
window shows the choices "1.⃖ 2.⃐ 3.⃔ 4.ˡ"; to choose "ˡ", I now type "4",<br>
and to choose "⃖", I now type "1".  Moreover, the package makes the last<br>
choice the current default.  Thus, after I type "⃔" with "\^l3", then<br>
"\^l[SPC]" inserts "⃔" into the buffer.<br>
<br>
Raghu.<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>>, <a href="http://www.retrotexts.net/" rel="noreferrer" target="_blank">http://www.retrotexts.net/</a><br>
Harish-Chandra Research Institute, <a href="http://www.hri.res.in/" rel="noreferrer" target="_blank">http://www.hri.res.in/</a><br>
</font></span><div class="HOEnZb"><div class="h5">______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>