[Agda] \^r

[Twan van Laarhoven]

ʳ can be entered as "\^r4". The default for "\^r" (i.e. "\^r1") is a combining 
right arrow. But you can browse between multiple symbols with the same escape 
code using the arrow keys or by entering a number. After that, this symbol 
becomes the default for "\^r".

Twan

On 20/12/13 14:01, Sergei Meshveliani wrote:
> People,
>
> Standard library lib-0.7  uses the symbol ʳ,  for example, in  _∷ʳ_.
>
> In emacs,  C-u C-x =   describes it as  "\^r"  and as  "upper 'r'".
>
> And when I type  \^r  under the agda mode in  emacs, my emacs prints a
> certain strange image, which under  C-u C-x =  is explained as
> whitespace  #x20.
>
> Meanwhile, I rename  ∷ʳ to ∷′  (\prime),  because it is difficult to
> copy ʳ by mouse each time.
>
> But may be someone knows how to fix the Agda Math mode respectively?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>