VScode user code snippets for Lean

lean.json

{
	"Type*": {
                "prefix": "Type*",
                "body": [
                  "{$1 : Type*}$0"
                ],
        "description": "Type* variable",
        },
        "Variables": {
                "prefix": "var",
                "body": [
                  "variables $0"
                ],
        "description": "Variables",
        },
        "Anonymous constructor": {
                "prefix": "constr",
                "body": [
                  "⟨$1⟩$0"
                ],
        "description": "Anonymous constructor",
        },
        "set_option": {
                "prefix": "#option",
                "body": [
                  "set_option $0"
                ],
        "description": "set_option",
        },
        "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",
        },
        "Lemma": {
                "prefix": "lemma",
                "body": [
                  "lemma $1 : $2 :=",
                  "$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"
	},
	"Split": {
        "prefix": "split",
        "body": [
		  "split,",
		  "{ $0",
		  "  sorry },",
		  "{ ",
		  "  sorry },"
        ],
        "description": "Split tactic"
        },
}