I am using the "Prettify Symbol Mode" extension and am getting wild behaviors: it overall works, but sometimes suddenly introduce symbols seemingly randomly, and I can't find how to fix it without closing the file.
I am for instance right now staring at a line devoid of any character, but displaying λ⇒≜←←, a "Lemma" displayed as the three dots of "Proof", the sequence of character "triv" in the middle of the name of a lemma displayed as "∀", among others...
Is the issue known, or am I missing something?
I think I tried it when first trying vscoq, but it certainly wasn't as good as company-coq. Since then I decided that writing things in unicode from the start is probably the better approach.
I don't disagree, but the primitives of the language and the standard library have not made this choice unfortunately
Yes… Anyway, I assume the issue is from the Prettify symbol side, isn't it?
If you require import
Utf8 you still get things like
Oh I actually didn't know of this module, thanks!
I'd still enjoy some prettification in the style of company-coq if that were possible I must say, but that's good to know :)
I opened an issue on the Github to raise the question.
Last updated: Jan 30 2023 at 18:04 UTC