Twan van Laarhoven
twanvl at gmail.com
Fri Dec 20 15:08:57 CET 2013
ʳ 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".
On 20/12/13 14:01, Sergei Meshveliani wrote:
> 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?
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda