[Agda] \^r
Sergei Meshveliani
mechvel at botik.ru
Fri Dec 20 14:01:52 CET 2013
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
More information about the Agda
mailing list