intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Consider showing math symbols instead of some language constructions

Open marat-rkh opened this issue 3 years ago • 1 comments

In Emacs mode for Coq (with company-coq), there is a special mode that shows math symbols instead of some language constructions, like lambdas, forall quantifier, etc.

With prettify-symbols-mode off: Screen Shot 2021-12-06 at 3 58 18 PM

With prettify-symbols-mode on: Screen Shot 2021-12-06 at 3 58 51 PM

We might try to add a similar feature to the plugin. Possible ways to do that include code foldings and Reader mode.

marat-rkh avatar Dec 06 '21 13:12 marat-rkh

I think that we might implement this feature similarly to how it is implemented in TexifyIDEA.

sxhya avatar Nov 06 '23 13:11 sxhya