Language specific ligatures for Dafny?

[cpitclaudel]

Hi Nikita, and thanks for Fira Code!

Would it be possible / easy to add support for language-specific ligatures for the Dafny language? I think the only two missing ligatures are :: (A notable difference from other languages is that the :: symbol is typically rendered as a centered dot in Dafny: ∙) and :- (to match :=). Context sensitive punctuation already takes care of :| it seems.

For reference, Dafny uses the following symbols:

->
~>
=>
-->
==>
<== 
<==>

<=
>=
==
!=

:=
:-
:|
::

!!
||
&&

Thanks!

[tonsky]

Hi! I can’t replace :: with single dot since it will confuse a lot of users in other context. :- is already in as cv26. We decided against enabling it by default as it might conflict with something like {x:-1}

[cpitclaudel]

Hi! I can’t replace :: with single dot since it will confuse a lot of users in other context.

Of course; I was hoping it might be possible to get an alternative for it, which would be disabled by default; would that be reasonable?

[tonsky]

Potentially yes. Let’s see how high the demand for it is.

By the way, when you say “the :: symbol is typically rendered as a centered dot in Dafny: ∙”, what exactly do you mean? Typically rendered where? How? Why replacement at all? Why just not use centered dot?

[cpitclaudel]

what exactly do you mean?

I mean in publications about the language, typically academic papers. Also in the emacs mode for Dafny, which uses Emacs' "prettification" feature to display :: as ∙ (and <= as ≤, etc.). It looks like this (above without "prettification", below with it):

Why replacement at all? Why just not use centered dot?

Mostly because it's harder to type in most editors than ::, I think.