Display keywords as Unicode mathematical symbols

[alex-chew]

Dafny users can have Emacs display certain keywords as Unicode mathematical symbols, like ∀ for forall: https://github.com/boogie-org/boogie-friends

It would be nice for the VSCode IDE to support this too.

[MikaelMayer]

I remember that we started to drop support for unicode mathematical symbols as Dafny is not targeted towards mathematicians but more engineers who are usually not used to typing and reading mathematical symbols in their code.

[kjx]

for what it's worth, I strongly suggest we don't do this.
Having "intense discussions" with Andrew Black over this regarding Grace,
I think expecting normal humans to write programs using characters that are not visible on their keyboards "will not help [adoption"...

[alex-chew]

In case I wasn't clear in my original comment, I wasn't suggesting that an option to display some keywords as Unicode symbols should be enabled by default.

[kjx]

that's fine. this is really just an excuse to post in pictures of daft keyboards.

now: export to LaTeX - that's a different matter...