[Agda] Superscript l and r in unicode

[Philip Wadler]

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/

[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" <***@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.

[N. Raghavendra]

Post by Philip Wadler
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.

[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/

Post by N. Raghavendra

Post by Philip Wadler
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.
--
Harish-Chandra Research Institute, http://www.hri.res.in/
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda