Valid but non-ascii identifiers are not processed?
Opened this issue · 0 comments
YaZko commented
A fairly niche shortcoming, but Coq allows for a little bit more than ASCII in identifiers, which VSCoq doesn't seem to take into account. For instance in the following minimal file, hovering over Y gives information about it, but not in the case of Xᵒ.
Definition Xᵒ : nat := 0.
Definition Y : nat := 1.
(* In the following, vscoq gives feedback about Y but not Xᵒ *)
Goal Y + Xᵒ = 1.