search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

U+02B3 (MODIFIER SMALL LETTER R, aka superscript r) not available via \^r #1001

Closed nrnrnr closed 3 months ago

nrnrnr commented 4 months ago

The text recommends using identifier that contain U+02B3 (ʳ). But using the agda-mode with version 2.6.3, the superscript r is not available using \^r as recommended. Instead this sequence produces a superscript right arrow.
Investigating turns up something wacky with the emacs mode located at /home/nr/.cabal/store/ghc-9.4.8/Agda-2.6.3-7fba3d17d3f11c4caee1846bd1530f2ccfa68d6deca502c7aef20d59e5478282/share/emacs-mode/agda2.el. In file agda-input.el, line 825 contains the pair

  ("^r"  . ,(agda-input-to-string-list"⃗⃑⃕"))

whereas line 1182 contains the pair

  ("^r" . ("ʳ"))

It appears that the former overrides the latter.

A similar issue applies to superscript l (ell).

wenkokke commented 4 months ago

This is an issue with Agda. Would you be willing to resubmit the issue upstream to the Agda repository?

wadler commented 4 months ago

Try using the arrow keys (or typing number keys). They should give you different superscript rightward arrows, and also superscript r. Go well, P

Sent from my iPhone

On 26 May 2024, at 18:23, Norman Ramsey @.***> wrote:

 This email was sent to you by someone outside the University. You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

The text recommends using identifier that contain U+02B3 (ʳ). But using the agda-mode with version 2.6.3, the superscript r is not available using \^r as recommended. Instead this sequence produces a superscript right arrow. Investigating turns up something wacky with the emacs mode located at /home/nr/.cabal/store/ghc-9.4.8/Agda-2.6.3-7fba3d17d3f11c4caee1846bd1530f2ccfa68d6deca502c7aef20d59e5478282/share/emacs-mode/agda2.el. In file agda-input.el, line 825 contains the pair

("^r" . ,(agda-input-to-string-list"⃗⃑⃕"))

whereas line 1182 contains the pair

("^r" . ("ʳ"))

It appears that the former overrides the latter.

A similar issue applies to superscript l (ell).

— Reply to this email directly, view it on GitHubhttps://github.com/plfa/plfa.github.io/issues/1001, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABFJ7MUPTSX66BVJTJEOAF3ZEID7LAVCNFSM6AAAAABIJ5PTCCVHI2DSMVQWIX3LMV43ASLTON2WKOZSGMYTOOBTGE3DONI. You are receiving this because you are subscribed to this thread.Message ID: @.***>

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

nrnrnr commented 4 months ago

Try using the arrow keys (or typing number keys). They should give you different superscript rightward arrows, and also superscript r.

Alas, @wadler, I'm offered a zillion arrows but no superscript r.

nrnrnr commented 4 months ago

@wenkokke would that be agda/agda?

nrnrnr commented 4 months ago

As per https://github.com/agda/agda/issues/7296, PLFA should update its instructions.

wenkokke commented 4 months ago

@nrnrnr Would you be willing to open a PR?