[Agda] arrow symbol

Serge D. Mechveliani mechvel at botik.ru
Mon Dec 31 18:45:46 CET 2012


People,
I thought that  ->  is equivalent to  \r

But now I observe that    cong : _*┬≥_ PreservesБ~~_ ->Б┴~~_ ->÷╤~~_Б┴┬_ 
is not type checked 
(I denote for this letter  * --> \. ,   ~~ --> \~~ ). 
And it is checked with  ->  replaced with  \r 
.
May be, it worths for the checker to automatically replace  ->  with  \r
just everywhere
(?)

Regards,

------
Sergei


More information about the Agda mailing list