[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