mechvel at botik.ru
Fri Dec 20 14:01:52 CET 2013
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
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?
More information about the Agda