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

[nrnrnr]

(This issue was previously reported at https://github.com/plfa/plfa.github.io/issues/1001, where it was recommended to be reported upstream.)

---

The text at https://github.com/plfa/plfa.github.io recommends using identifiers that contain U+02B3 (ʳ). But using the Emacs 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 strange with the emacs mode. 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).

This report applies to version 2.6.3, but a quick download of the current HEAD suggests that commit 5f366190b3d0eeebc91514d6ec60f8fa06e72708 may have the same issue.

I'm using Agda 2.6.3 with Emacs 28. Compiled with GHC 2.4.8.

[JacquesCarette]

It is available as \r4 as there are in fact 4 things bound to \r (as can be seen in the input buffer). That the superscript right-arrow is first is kind of annoying as I tend to use U+02B3 (ʳ) way more. But once you've used \r4 once, then it defaults to that within the rest of that session.

(But this might be a new problem with Emacs 28?)

[nrnrnr]

@JacquesCarette On my installation \r4 produces ⭆. Inspecting the source code of both versions, I can't see that HEAD is likely to be different.

[JacquesCarette]

Oops: \^r4 forgot the ^.

[nrnrnr]

@JacquesCarette Bingo! Thank you.