Add some basic snippets

[eric-wieser]

Not sure if these are really all that useful, but though I'd suggest them anyway.

[gebner]

I think these could prove to be fairly controversial. You automatically get a lot of text when you type structure. I don't see an easy way to avoid the snippets since you need to type structure as a keyword. Can we add an options in the settings to enable them?

Note that it's also possible to add the snippets to e.g. mathlib.

[eric-wieser]

I don't see an easy way to avoid the snippets since you need to type structure as a keyword. Can we add an options in the settings to enable them?

vscode lets you pick between the two options, and uses your last choice as a default:

[eric-wieser]

Can we add an options in the settings to enable them?

We could, but there are already extensions to manage unwanted snippets like https://github.com/svipas/vscode-control-snippets. microsoft/vscode#10565 is related.

[gebner]

Ok, so I've tried them out a bit.

• They are not triggered automatically unless you explicitly select them in the dropdown. This is good.
• The structure snippet does not follow the mathlib style guide. The := should be at the end of the first line. The fields should not be indented.
• The input abbreviation does not work in snippets. That is, you can't type \nat in a snippet field. 😭
• I'm not sure how much they help. The lean syntax does not have much boilerplate. At best I don't have to type := but that's it.

I've posted a thread in the PR reviews stream on zulip.

[utensil]

The lines below are a little too much. structure should not make too much assumption on the organization after the structure. If this snippet is called theory for boilerplate of developing a theory, maybe it would be OK but there would be much more.

[utensil]

Usually variables should be declared in a named section.

[bryangingechen]

Declaring variables in a namespace is fine too.