Suggest adding a .vscode/settings.json

[kim-em]

Many Lean projects have a .vscode/settings.json:

{
  "editor.insertSpaces": true,
  "editor.tabSize": 2,
  "editor.rulers" : [100],
  "files.encoding": "utf8",
  "files.eol": "\n",
  "files.insertFinalNewline": true,
  "files.trimFinalNewlines": true,
  "files.trimTrailingWhitespace": true,
}

These do some basic file normalization that makes life easier in git, and encourages basic stylistic compatibility with other Lean projects.

Could the VSCode extension notice that a project doesn't have this file, and suggest adding this one?

[mhuisi]

It could. I'm not sure whether a suggestion is the best way to go about this though - I usually find these very annoying in other extensions.

For a first step, we could generate it when creating a new project using the corresponding VSCode command that will be added for #61 and give users access to generate a sensible default config using a separate VSCode command.

[kim-em]

Agree the suggestion could be annoying. But without a suggestion it probably won't get that much uptake. Low priority then, unless we find this is a persistent problem.