Zulip Chat Archive

Stream: new members

Topic: noob VS Code autocomplete question


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 16 2019 at 13:52):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 13:58):

happens to me all the time

view this post on Zulip Marc Huisinga (Nov 16 2019 at 13:59):

pretty sure that has happened to me before as well

view this post on Zulip Wojciech Nawrocki (Nov 16 2019 at 14:03):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 14:03):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 14:07):

Increasing "Editor: Quick Suggestions Delay" might also help

view this post on Zulip Mario Carneiro (Nov 16 2019 at 14:10):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 16 2019 at 14:19):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 14:21):

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

view this post on Zulip Mario Carneiro (Nov 16 2019 at 14:21):

10 millisecond delay is the default, which is almost nothing

view this post on Zulip 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