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_lean.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
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
let lang_id = "lean"
let json = {json|{
  "displayName": "Lean 4",
  "fileTypes": [
  ],
  "name": "lean",
  "patterns": [
    {
      "include": "#comments"
    },
    {
      "match": "\\b(Prop|Type|Sort)\\b",
      "name": "storage.type.lean4"
    },
    {
      "captures": {
        "1": {
          "name": "storage.modifier.lean4"
        },
        "2": {
          "name": "storage.modifier.lean4"
        },
        "3": {
          "name": "storage.modifier.lean4"
        }
      },
      "match": "\\b(attribute\\b\\s*)(?:(\\[[^]\\s]*])|\\[([^]\\s]*))"
    },
    {
      "captures": {
        "1": {
          "name": "storage.modifier.lean4"
        },
        "2": {
          "name": "storage.modifier.lean4"
        },
        "3": {
          "name": "storage.modifier.lean4"
        }
      },
      "match": "(@)(?:(\\[[^]\\s]*])|\\[([^]\\s]*))"
    },
    {
      "match": "\\b(?<!\\.)(local|scoped|partial|unsafe|nonrec|public|private|protected|noncomputable|meta)(?!\\.)\\b",
      "name": "storage.modifier.lean4"
    },
    {
      "match": "\\b(sorry|admit|#exit)\\b",
      "name": "invalid.illegal.lean4"
    },
    {
      "match": "#(print|eval!??|reduce|synth|widget|where|version|with_exporting|check|check_tactic|check_tactic_failure|check_failure|check_simp|discr_tree_key|discr_tree_simp_key|guard|guard_expr|guard_msgs)\\b",
      "name": "keyword.other.lean4"
    },
    {
      "match": "\\bderiving\\s+instance\\b",
      "name": "keyword.other.command.lean4"
    },
    {
      "begin": "\\b(?<!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class)\\b\\s+(\\{[^}]*})?",
      "beginCaptures": {
        "1": {
          "name": "keyword.other.definitioncommand.lean4"
        }
      },
      "end": "(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[(:<>\\[{|⦃])",
      "name": "meta.definitioncommand.lean4",
      "patterns": [
        {
          "include": "#comments"
        },
        {
          "include": "#definitionName"
        },
        {
          "match": ","
        }
      ]
    },
    {
      "match": "\\b(?<!\\.)(theorem|show|have|using|haveI|from|suffices|nomatch|nofun|no_index|def|class|structure|instance|elab|set_option|initialize|builtin_initialize|example|inductive_fixpoint|inductive|coinductive_fixpoint|coinductive|termination_by\\??|decreasing_by|partial_fixpoint|axiom|universe|variable|module|import all|import|open|export|prelude|renaming|hiding|do|by\\??|letI??|let_expr|extends|mutual|mut|where|rec|declare_syntax_cat|syntax|macro_rules|macro|binop_lazy%|binop%|unop%|binrel_no_prop%|binrel%|leftact%|rightact%|max_prec|leading_parser|elab_rules|deriving|fun|section|namespace|end|prefix|postfix|infixl|infixr?|notation|abbrev|if|bif|then|else|calc|matches|match_expr|match|with|forall|for|while|repeat|unless|until|panic!|unreachable!|assert!|try|catch|finally|return|continue|break|exists|mod_cast|exact\\?%|include_str|include|in|trailing_parser|tactic_tag|tactic_alt|tactic_extension|register_tactic_tag|type_of%|binder_predicate|grind_propagator|builtin_grind_propagator|grind_pattern|simproc|builtin_simproc|simproc_pattern%|builtin_simproc_pattern%|simproc_decl|builtin_simproc_decl|dsimproc|builtin_dsimproc|dsimproc_decl|builtin_dsimproc_decl|show_panel_widgets|show_term|seal|unseal|nat_lit|norm_cast_add_elim|println!|private_decl%|declare_config_elab|decl_name%|register_error_explanation|register_builtin_option|register_option|register_parser_alias|register_simp_attr|register_linter_set|register_label_attr|recommended_spelling|reportIssue!|reprove|run_elab|run_cmd|run_meta|value_of%|add_decl_doc|omit|opaque|json%|dbg_trace|trace_goal\\[[^]\\s]*]|trace\\[[^]\\s]*]|throwErrorAt|throwError|throwNamedErrorAt|throwNamedError|logNamedWarningAt|logNamedWarning|logNamedErrorAt|logNamedError)(?!\\.)\\b",
      "name": "keyword.other.lean4"
    },
    {
      "begin": "«",
      "contentName": "entity.name.lean4",
      "end": "»"
    },
    {
      "begin": "(s!|m!|throwError|dbg_trace|panic!|reportIssue!|trace(?:_goal|)\\[[^]\\s]*])\\s*\"",
      "beginCaptures": {
        "1": {
          "name": "keyword.other.lean4"
        }
      },
      "end": "\"",
      "name": "string.interpolated.lean4",
      "patterns": [
        {
          "begin": "(\\{)",
          "beginCaptures": {
            "1": {
              "name": "keyword.other.lean4"
            }
          },
          "end": "(})",
          "endCaptures": {
            "1": {
              "name": "keyword.other.lean4"
            }
          },
          "patterns": [
            {
              "include": "$self"
            }
          ]
        },
        {
          "match": "\\\\[\"'\\\\nrt]",
          "name": "constant.character.escape.lean4"
        },
        {
          "match": "\\\\x\\h\\h",
          "name": "constant.character.escape.lean4"
        },
        {
          "match": "\\\\u\\h\\h\\h\\h",
          "name": "constant.character.escape.lean4"
        }
      ]
    },
    {
      "begin": "\"",
      "end": "\"",
      "name": "string.quoted.double.lean4",
      "patterns": [
        {
          "match": "\\\\[\"'\\\\nrt]",
          "name": "constant.character.escape.lean4"
        },
        {
          "match": "\\\\x\\h\\h",
          "name": "constant.character.escape.lean4"
        },
        {
          "match": "\\\\u\\h\\h\\h\\h",
          "name": "constant.character.escape.lean4"
        }
      ]
    },
    {
      "match": "\\b(true|false)\\b",
      "name": "constant.language.lean4"
    },
    {
      "match": "(?<![]\\w])'[^'\\\\]'",
      "name": "string.quoted.single.lean4"
    },
    {
      "captures": {
        "1": {
          "name": "constant.character.escape.lean4"
        }
      },
      "match": "(?<![]\\w])'(\\\\(x\\h\\h|u\\h\\h\\h\\h|.))'",
      "name": "string.quoted.single.lean4"
    },
    {
      "match": "\\b([0-9]+|0([Xx]\\h+)|-?(0|[1-9][0-9]*)(\\.[0-9]+)?([Ee][-+]?[0-9]+)?)\\b",
      "name": "constant.numeric.lean4"
    }
  ],
  "repository": {
    "blockComment": {
      "begin": "/-",
      "end": "-/",
      "name": "comment.block.lean4",
      "patterns": [
        {
          "include": "source.lean4.markdown"
        },
        {
          "include": "#blockComment"
        }
      ]
    },
    "comments": {
      "patterns": [
        {
          "include": "#dashComment"
        },
        {
          "include": "#docComment"
        },
        {
          "include": "#modDocComment"
        },
        {
          "include": "#blockComment"
        }
      ]
    },
    "dashComment": {
      "begin": "--",
      "end": "$",
      "name": "comment.line.double-dash.lean4",
      "patterns": [
        {
          "include": "source.lean4.markdown"
        }
      ]
    },
    "definitionName": {
      "patterns": [
        {
          "match": "\\b[^():=?{}«»λ→∀\\s][^():{}«»\\s]*",
          "name": "entity.name.function.lean4"
        },
        {
          "begin": "«",
          "contentName": "entity.name.function.lean4",
          "end": "»"
        }
      ]
    },
    "docComment": {
      "begin": "/--",
      "end": "-/",
      "name": "comment.block.documentation.lean4",
      "patterns": [
        {
          "include": "source.lean4.markdown"
        },
        {
          "include": "#blockComment"
        }
      ]
    },
    "modDocComment": {
      "begin": "/-!",
      "end": "-/",
      "name": "comment.block.documentation.lean4",
      "patterns": [
        {
          "include": "source.lean4.markdown"
        },
        {
          "include": "#blockComment"
        }
      ]
    }
  },
  "scopeName": "source.lean4"
}|json}