Zulip Chat Archive

Stream: PR reviews

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


view this post on Zulip Gabriel Ebner (Jul 27 2020 at 12:20):

@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?

view this post on Zulip Patrick Massot (Jul 27 2020 at 12:38):

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"
        }
}

view this post on Zulip Utensil Song (Jul 27 2020 at 13:38):

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.


Last updated: May 09 2021 at 12:14 UTC