Consider adding a completion for unicode symbols in aliases

[marat-rkh]

Suppose I am writing the following declaration:

\data Term
  | ref Id
  | lam Id Term
  | app \alias \infixl 7 {-caret-} Term Term

I want to add ∙ alias for app. The IDE doesn't help me with this.

1. To add the alias I have to open Unicode symbols table somewhere externally.
2. Sometimes, the symbol I find is invalid, because Arend allows a restricted set of them in aliases.

I think this can be addressed by adding a completion. For this particular case, the completion item would be called bullet or bullet_point (this is the name of the ∙ symbol in the Unicode table). When you select it, it inserts ∙.

[valis]

This is actually kind of the point. We allow a restricted range of Unicode symbols because otherwise there will be a large number of incomprehensible and almost identical ones. We may enlarge the allowed set, but we need to choose new symbols carefully. I think we already discussed this somewhere and I even gave a list of possible candidates. Anyway, here it is again:

Arrows 2190-21FF
Leterlike Symbols 2100-214F
Miscellaneous Methematical Symbols_A 27C0-27EF
Suplemental Arrows_A 27F0-27FF
Suplemental Arrows_B 2900-297F
Miscellaneous Methematical Symbols_B 2980-29FF
Supplemental Mathematical Operators 2A00-2AFF
Mathematical Alphanumeric Symbols 1D400-1D7FF

We don't have any completion for Unicode symbols in declarations basically for the same reason. It should be easy to use them (and it is), but not that easy to declare them, so that they won't be overused.

[marat-rkh]

Yeah, we have talked about adding more symbols here: https://github.com/JetBrains/Arend/issues/299

Speaking of completion. Do I get it correctly that you would avoid adding it completely?

[valis]

Do I get it correctly that you would avoid adding it completely?

That was the initial intent. I'm not strongly against it, but I think we can keep it at that for the time being.

[marat-rkh]

Ok, got your point)

[sxhya]

@valis Is your last commit 07894de712c37442310d1522d23eb907e108b145 related to this issue? Can it be closed?