Open fweth opened 1 year ago
Hi, it seems like the extension doesn't change VSCode's "highlight ambiguous characters" feature. It's not a big deal since you can disable the feature manually for certain languages, but other extensions, like Lean4, seem to do that automatically.
Hi, it seems like the extension doesn't change VSCode's "highlight ambiguous characters" feature. It's not a big deal since you can disable the feature manually for certain languages, but other extensions, like Lean4, seem to do that automatically.