[Agda] Superscript l and r in unicode

[Philip Wadler]

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

.   \ 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/

On 10 February 2018 at 02:59, N. Raghavendra <nyraghu27132 at gmail.com> wrote:

> 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/
> _______________________________________________
> 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/20180210/90c1de3c/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180210/90c1de3c/attachment.ksh>