noob VS Code autocomplete question

Stream: new members

[Kevin Buzzard]

I have some really stupid option set on VS Code. If I type

def hi (a b : ℕ) : Prop := a = b

in the first line of a VS Code .lean file, and then hit "enter" or "return" or whatever it's called nowadays, the b changes to begin. Why would I want that to happen? Would I be better off changing this option somehow? It frustrates me.

[Kevin Buzzard]

Am I the only person this happens to, by the way?

[Mario Carneiro]

happens to me all the time

[Marc Huisinga]

pretty sure that has happened to me before as well

[Wojciech Nawrocki]

You can turn this off in the Editor: Accept Suggestion On Enter setting

[Mario Carneiro]

I think the relevant categories are "Editor › Suggest: Show Keywords" and "Editor › Suggest: Show Words"

[Mario Carneiro]

Increasing "Editor: Quick Suggestions Delay" might also help

[Mario Carneiro]

I can't find a setting to turn off auto activation on writing letters though

[Mario Carneiro]

aha, you have to write it in json but "editor.quickSuggestions": false turns autocomplete off except via ctrl-space

[Johan Commelin]

I also have this issue with enter after . in docstrings and comments.

[Johan Commelin]

I would prefer to have quickSuggestion after typing at least two letters. That would solve the = b-enter problem

[Mario Carneiro]

I think adding a delay is the easiest way to handle the single letter problem

[Mario Carneiro]

10 millisecond delay is the default, which is almost nothing

[Mario Carneiro]

200 ms should be more than enough for a reasonable typing speed