agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

Published 20 hours ago • verified publisher icon banacorn

Built-in sorts are highlighted as strings

Open fredrik-bakke opened this issue 10 months ago • 1 comments

Built-in sorts are highlighted as strings, but shouldn't be: image I suggest using a scope like support.type.sort.agda instead.

fredrik-bakke avatar Aug 24 '23 08:08 fredrik-bakke