Coq Commands.sublime-completions

{
  "scope": "source.coq",

  "completions":
  [
    { "trigger": "Inductive", "contents": "Inductive $1 : Type :=\n  | $0." },
    { "trigger": "Definition", "contents": "Definition $1 :=\n  $0." },
    { "trigger": "Fixpoint", "contents": "Fixpoint $1 :=\n  $0." },
    { "trigger": "Proof", "contents": "Proof. $0" },
    { "trigger": "Check", "contents": "Check $0." },
    { "trigger": "Eval", "contents": "Eval $1 in $0." },
    { "trigger": "Notation", "contents": "Notation \"$1\" := $2\n  (at level $3, $4 associativity)\n  : $5_scope." },

    { "trigger": "Example", "contents": "Example $1 : $2.\nProof.\n  $0\nQed." },
    { "trigger": "Theorem", "contents": "Theorem $1 : $2.\nProof.\n  $0\nQed." },
    { "trigger": "Lemma", "contents": "Lemma $1 : $2.\nProof.\n  $0\nQed." },
    { "trigger": "Fact", "contents": "Fact $1 : $2.\nProof.\n  $0\nQed." },
    { "trigger": "Remark", "contents": "Remark $1 : $2.\nProof.\n  $0\nQed." },

    { "trigger": "Section", "contents": "Section $1.\n\n$0\n\nEnd $1." },

    { "trigger": "forall", "contents": "forall $1: $2, $0" },
    { "trigger": "exists", "contents": "exists $1, $0" },
    { "trigger": "fun", "contents": "fun (${1:x}:${2:type}) => ${0:body}" },
    { "trigger": "if", "contents": "if ${1:bool} then $2 else $3" },
    { "trigger": "match", "contents": "match $1 with\n| $2 => $3\nend" }
  ]
}