## Stream: new members

### Topic: noob VS Code autocomplete question

#### Kevin Buzzard (Nov 16 2019 at 13:51):

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 (Nov 16 2019 at 13:52):

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

#### Mario Carneiro (Nov 16 2019 at 13:58):

happens to me all the time

#### Marc Huisinga (Nov 16 2019 at 13:59):

pretty sure that has happened to me before as well

#### Wojciech Nawrocki (Nov 16 2019 at 14:03):

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

#### Mario Carneiro (Nov 16 2019 at 14:03):

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

#### Mario Carneiro (Nov 16 2019 at 14:07):

Increasing "Editor: Quick Suggestions Delay" might also help

#### Mario Carneiro (Nov 16 2019 at 14:10):

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

#### Mario Carneiro (Nov 16 2019 at 14:18):

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

#### Johan Commelin (Nov 16 2019 at 14:19):

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

#### Johan Commelin (Nov 16 2019 at 14:20):

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

#### Mario Carneiro (Nov 16 2019 at 14:21):

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

#### Mario Carneiro (Nov 16 2019 at 14:21):

10 millisecond delay is the default, which is almost nothing

#### Mario Carneiro (Nov 16 2019 at 14:22):

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

Last updated: May 08 2021 at 09:11 UTC