leanprover/vscode-lean#214 snippets for `def`, etc.

Stream: PR reviews

[Gabriel Ebner]

@Eric Wieser has proposed some snippets for declarations like def, etc. I'm not sure how much they would help in practice.
What are your thoughts on the snippets in leanprover/vscode-lean#214?
Are there any snippets that would make your life easier?

[Patrick Massot]

It seems this list is disjoint from I find useful. The snippets I use are:

{
    "Type*": {
                "prefix": "Type*",
                "body": [
                  "{$1 : Type*}$0"
                ],
        "description": "Type* variable",
        },
        "Variables": {
                "prefix": "var",
                "body": [
                  "variables $0"
                ],
        "description": "Variables",
        },
        "set_option pp.implicit": {
                "prefix": "#implicit",
                "body": [
                  "set_option pp.implicit true$0"
                ],
        "description": "Pretty print implicit",
        },
        "set_option pp.all": {
                "prefix": "#all",
                "body": [
                  "set_option pp.all true$0"
                ],
        "description": "Pretty print all",
        },
        "Trace instance": {
                "prefix": "#instance",
                "body": [
                  "set_option trace.class_instances true$0"
                ],
        "description": "Trace class instances",
        },
        "Trace simp rewrite": {
                "prefix": "#rewrite",
                "body": [
                  "set_option trace.simplify.rewrite true$0"
                ],
        "description": "Trace simp rewrites",
        },
        "Sorry": {
        "prefix": "sor",
        "body": [
          "{ $0",
          "  sorry },"
        ],
        "description": "Sorry block"
    },
    "Proof": {
        "prefix": "proof",
        "body": [
          "begin",
          "  $0",
          "  sorry",
          "end",
        ],
        "description": "Proof tactic block"
    },
    "Library search": {
        "prefix": "LS",
        "body": [
          "library_search,",
        ],
        "description": "Library search"
    },
    "Split": {
        "prefix": "split",
        "body": [
          "split,",
          "{ $0",
          "  sorry },",
          "{ ",
          "  sorry },"
        ],
        "description": "Split tactic"
        },
        "Anonymous_constructor" : {
                "prefix": "ac",
                "body": ["⟨$0⟩"],
                "description": "Insert anonymous constructor"
        }
}

[Utensil Song]

The expectation of having such snippets is from other programming languages but @Gabriel Ebner makes a good point:

The lean syntax does not have much boilerplate. At best I don't have to type := but that's it.

and "The input abbreviation does not work in snippets" makes the holes like ${1:hole_name} less useful.

Mostly only pairing snippets are useful such as namespace, section, Patrick's proof, split, sorry, ac.

The ones for options are great too, it would be better if they share the same unused prefix.

var is mostly useless because the problem is actually the annoying singular variable, so a word with a different prefix is needed here such as vs. Type* contains too many keystrokes(involving Shift) to be generally convenient.