Automatic tactic suggestions in VS Code: useful or harmful?

Stream: new members

[İmran Tanrikolu]

Hi everyone, I’m learning Lean in VS Code and I noticed something: when I write an example with := by sorry, VS Code sometimes gives me automatic tactic suggestions. If I press the tab key, it fills in the proof steps for me. I was wondering: is this feature meant to be used regularly, or is it more like a learning aid? Do you think relying on it is harmful for actually learning how to write proofs in Lean? Also, where exactly can I enable or disable this feature in the VS Code settings?

[Kevin Buzzard]

Are you talking about copilot? Disable it in bottom right? This is not Lean-specific.

[İmran Tanrikolu]

No, not Copilot. I think it’s a feature within Lean itself, called “automatic tactic suggestions,” though I might be mistaken.

[Kenny Lau]

the light bulb?

[İmran Tanrikolu]

I just checked, and it turns out the suggestions were from Copilot. Do you think using this would be helpful during the learning phase?

[Aaron Liu]

I would say don't use copilot unless you know what it's doing

[İmran Tanrikolu]

Thank you for your responses.