vscode-lean4
vscode-lean4 copied to clipboard
Autocompletion after inputting an underscore
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.