snippets

Stream: general

[Kevin Buzzard]

Can I use "snippets" to change

      blah,
      split,
      sorry
    },

(which suddenly now errors because the tactic split just created two subgoals) to

      blah
      split,
      {
        sorry
      },
      {
        sorry
      }
    },

? Patrick might even have shown me how to do this once before, but I want to get into the habit of using it so I can stream well-parenthesized code as flluently as possible.

[Shing Tak Lam]

Something like this in your snippets file should work

    "Split": {
      "prefix": "split",
      "body": [
        "split,",
        "  { sorry },",
        "  { sorry },",
      ],
      "description": "Split"
    }

[Kevin Buzzard]

Wait no, this would only trigger on split. I want a bifurcate_goal snippet which changes one sorry to two. I see the syntax now though. Thanks.

[Kevin Buzzard]

If you keep the last line of your proof a bare sorry and end every tactic with a comma, then the snippet I want enables you to seamlessly continue in the same format with no errors.