package tm-grammars

  1. Overview
  2. Docs
package tm-grammars
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file tm_grammar_coq.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
let lang_id = "coq"
let json = {json|{
  "displayName": "Coq",
  "fileTypes": [
    "v"
  ],
  "name": "coq",
  "patterns": [
    {
      "match": "\\b(From|Require|Import|Export|Local|Global|Include)\\b",
      "name": "keyword.control.import.coq"
    },
    {
      "match": "\\b((Open|Close|Delimit|Undelimit|Bind)\\s+Scope)\\b",
      "name": "keyword.control.import.coq"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "2": {
          "name": "entity.name.function.theorem.coq"
        }
      },
      "match": "\\b(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition)\\s+(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "match": "\\bGoal\\b",
      "name": "keyword.source.coq"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "2": {
          "name": "keyword.source.coq"
        },
        "3": {
          "name": "entity.name.assumption.coq"
        }
      },
      "match": "\\b(Parameters?|Axioms?|Conjectures?|Variables?|Hypothesis|Hypotheses)(\\s+Inline)?\\b\\s*\\(?\\s*(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "3": {
          "name": "entity.name.assumption.coq"
        }
      },
      "match": "\\b(Context)\\b\\s*`?\\s*([({])?\\s*(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "2": {
          "name": "keyword.source.coq"
        },
        "3": {
          "name": "entity.name.function.coq"
        }
      },
      "match": "(\\b(?:Program|Local)\\s+)?\\b(Definition|Fixpoint|CoFixpoint|Function|Example|Let(?:(?:\\s+|\\s+Co)Fixpoint)?|Instance|Equations|Equations?)\\s+(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        }
      },
      "match": "\\b((Show\\s+)?Obligation\\s+Tactic|Obligations\\s+of|Obligation|Next\\s+Obligation(\\s+of)?|Solve\\s+Obligations(\\s+of)?|Solve\\s+All\\s+Obligations|Admit\\s+Obligations(\\s+of)?|Instance)\\b"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "3": {
          "name": "entity.name.type.coq"
        }
      },
      "match": "\\b(CoInductive|Inductive|Variant|Record|Structure|Class)\\s+(>\\s*)?(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "2": {
          "name": "entity.name.function.ltac"
        }
      },
      "match": "\\b(Ltac)\\s+(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "captures": {
        "1": {
          "name": "keyword.source.coq"
        },
        "2": {
          "name": "keyword.source.coq"
        },
        "3": {
          "name": "entity.name.function.ltac"
        }
      },
      "match": "\\b(Ltac2)\\s+(mutable\\s+)?(rec\\s+)?(([_ \\p{L}])(['0-9_ \\p{L}])*)"
    },
    {
      "match": "\\b(Hint(\\s+Mode)?|Create\\s+HintDb|Constructors|Resolve|Rewrite|Ltac2??|Implicit(\\s+Types)?|Set|Unset|Remove\\s+Printing|Arguments|((Tactic|Reserved)\\s+)?Notation|Infix|Section|Module(\\s+Type)?|End|Check|Print(\\s+All)?|Eval|Compute|Search|Universe|Coercions|Generalizable(\\s+(All|Variable))?|Existing(\\s+(Class|Instance))?|Canonical|About|Locate|Collection|Typeclasses\\s+(Opaque|Transparent))\\b",
      "name": "keyword.source.coq"
    },
    {
      "match": "\\b(Proof|Qed|Defined|Save|Abort(\\s+All)?|Undo(\\s+To)?|Restart|Focus|Unfocus|Unfocused|Show\\s+Proof|Show\\s+Existentials|Show|Unshelve)\\b",
      "name": "keyword.source.coq"
    },
    {
      "match": "\\b(Quit|Drop|Time|Redirect|Timeout|Fail)\\b",
      "name": "keyword.debug.coq"
    },
    {
      "match": "\\b(admit|Admitted)\\b",
      "name": "invalid.illegal.admit.coq"
    },
    {
      "match": "[-*+:<=>{|}¬→↔∧∨≠≤≥]",
      "name": "keyword.operator.coq"
    },
    {
      "match": "\\b(forall|exists|Type|Set|Prop|nat|bool|option|list|unit|sum|prod|comparison|Empty_set)\\b|[∀∃]",
      "name": "support.type.coq"
    },
    {
      "match": "\\b(try|repeat|rew|progress|fresh|solve|now|first|tryif|at|once|do|only)\\b",
      "name": "keyword.control.ltac"
    },
    {
      "match": "\\b(into|with|eqn|by|move|as|using)\\b",
      "name": "keyword.control.ltac"
    },
    {
      "match": "\\b(match|lazymatch|multimatch|match!|lazy_match!|multi_match!|fun|with|return|end|let|in|if|then|else|fix|for|where|and)\\b|λ",
      "name": "keyword.control.gallina"
    },
    {
      "match": "\\b(intros??|revert|induction|destruct|auto|eauto|tauto|eassumption|apply|eapply|assumption|constructor|econstructor|reflexivity|inversion|injection|assert|split|esplit|omega|fold|unfold|specialize|rewrite|erewrite|change|symmetry|refine|simpl|intuition|firstorder|generalize|idtac|exists??|eexists|elim|eelim|rename|subst|congruence|trivial|left|right|set|pose|discriminate|clear|clearbody|contradict|contradiction|exact|dependent|remember|case|easy|unshelve|pattern|transitivity|etransitivity|f_equal|exfalso|replace|abstract|cycle|swap|revgoals|shelve|unshelve)\\b",
      "name": "support.function.builtin.ltac"
    },
    {
      "applyEndPatternLast": 1,
      "begin": "\\(\\*(?!#)",
      "end": "\\*\\)",
      "name": "comment.block.coq",
      "patterns": [
        {
          "include": "#block_comment"
        },
        {
          "include": "#block_double_quoted_string"
        }
      ]
    },
    {
      "match": "\\b((0([Xx])\\h+)|([0-9]+(\\.[0-9]+)?))\\b",
      "name": "constant.numeric.gallina"
    },
    {
      "match": "\\b(True|False|tt|false|true|Some|None|nil|cons|pair|inl|inr|[OS]|Eq|Lt|Gt|id|ex|all|unique)\\b",
      "name": "constant.language.constructor.gallina"
    },
    {
      "match": "\\b_\\b",
      "name": "constant.language.wildcard.coq"
    },
    {
      "begin": "\"",
      "beginCaptures": {
        "0": {
          "name": "punctuation.definition.string.begin.coq"
        }
      },
      "end": "\"",
      "endCaptures": {
        "0": {
          "name": "punctuation.definition.string.end.coq"
        }
      },
      "name": "string.quoted.double.coq"
    }
  ],
  "repository": {
    "block_comment": {
      "applyEndPatternLast": 1,
      "begin": "\\(\\*(?!#)",
      "end": "\\*\\)",
      "name": "comment.block.coq",
      "patterns": [
        {
          "include": "#block_comment"
        },
        {
          "include": "#block_double_quoted_string"
        }
      ]
    },
    "block_double_quoted_string": {
      "applyEndPatternLast": 1,
      "begin": "\"",
      "beginCaptures": {
        "0": {
          "name": "punctuation.definition.string.begin.coq"
        }
      },
      "end": "\"",
      "endCaptures": {
        "0": {
          "name": "punctuation.definition.string.end.coq"
        }
      },
      "name": "string.quoted.double.coq"
    }
  },
  "scopeName": "source.coq"
}|json}