Discussion:
Superscript l and r in unicode
(too old to reply)
Philip Wadler
2018-02-08 21:36:13 UTC
Permalink
Raw Message
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ő
2018-02-09 05:47:14 UTC
Permalink
Raw Message
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
2018-02-10 06:59:53 UTC
Permalink
Raw Message
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.
--
N. Raghavendra <***@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
Philip Wadler
2018-02-10 12:35:32 UTC
Permalink
Raw Message
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
Loading...