Open andreasabel opened 6 years ago
It is very basic. You move your cursor over the position you want to apply a hint and then press the key combination which then performs the hint.
For complicated files with CPP in this might fail silently.
Is there something in particular you are having problems with?
Well, I do not even see any hints I could apply. I would have expected some kind of visualization where hints can be applied. It seems like I have to do this workflow:
C-c , r
Is that correct?
(And, as you said for complicated files with CPP
it does not do anything anyway. I guess 90% of Agda's source files fall in this category.)
Please detail a bit in the README how this mode is supposed to be used. What is the workflow? A walk through by example would be nice.