vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Autocompletion after inputting an underscore

Open javra opened this issue 3 years ago • 4 comments

I noticed that the autocompletion box opens whenever I want to input a placeholder _, which is pretty annoying. It offers me to complete to _law, of which I have no idea where it comes from.

javra avatar Mar 12 '21 12:03 javra