{"name":"F*","scopeName":"source.fstar","patterns":[{"include":"#comments"},{"include":"#modules"},{"include":"#options"},{"include":"#expr"}],"repository":{"commentblock":{"patterns":[{"name":"comment.block.fstar","begin":"\\(\\*","end":"\\*\\)","patterns":[{"include":"#commentblock"}],"beginCaptures":{"0":{"name":"punctuation.definition.comment.begin.fstar"}},"endCaptures":{"0":{"name":"punctuation.definition.comment.end.fstar"}}}]},"comments":{"patterns":[{"name":"comment.line.fstar","match":"//.*"},{"include":"#commentblock"}]},"expr":{"patterns":[{"include":"#comments"},{"name":"variable.other.generic-type.fstar","match":"'[a-zA-Z0-9_]+\\b"},{"include":"#strings"},{"name":"support.class.base.fstar","match":"\\b(int|nat|pos|bool|unit|string|Type|Type0|eqtype)\\b"},{"name":"support.class.base.fstar","match":"(/\\\\|\\\\/|\u003c:|\u003c@|[(][|]|[|][)]|u#|~\u003e|-\u003e|\u003c--|\u003c-|\u003c==\u003e|==\u003e|[?][.]|[.]\\[|[.]\\(|[{][:]pattern|::|:=|;;|[!][{]|\\[[|]|[|]\u003e|[|]\\]|[~+^\u0026?$|#,.:;=\\[\\](){}-])"},{"name":"constant.language.monad.fstar","match":"\\b(Pure|PURE|Tot|STATE|ST|St|Stack|StackInline|HST|ALL|All|EXN|Exn|Ex|DIV|Div|GHOST|Ghost|GTot|Lemma)\\b"},{"name":"constant.language.fstar","match":"\\b(_|[(]\\s*[)]|\\[\\s*\\])\\b"},{"name":"keyword.other.fstar","match":"\\b(let|in|type|kind|val|rec|and|if|then|else|assume|admit|assert|assert_norm|squash|failwith|SMTPat|SMTPatOr|hasEq|fun|function|forall|exists|exception|by|new_effect|reify|try|synth|with|when)\\b"},{"name":"storage.modifier.fstar","match":"\\b(abstract|attributes|noeq|unopteq|inline|inline_for_extraction|irreducible|logic|mutable|new|noextract|private|reifiable|reflectable|total|unfold|unfoldable)\\b"},{"name":"constant.language.boolean.fstar","match":"\\b([tT]rue|[fF]alse)\\b"},{"name":"constant.numeric.hex.js","match":"\\b0[xX][0-9a-fA-F]+[uU]?[zyslL]?\\b"},{"name":"constant.numeric.decimal.js","match":"\\b[0-9]+[uU]?[zyslL]?\\b"},{"match":"(?x)\n(?:\n  (?:\\b[0-9]+(\\.)[0-9]+[eE][+-]?[0-9]+\\b)| # 1.1E+3\n  (?:\\b[0-9]+(\\.)[eE][+-]?[0-9]+\\b)|       # 1.E+3\n  (?:\\B(\\.)[0-9]+[eE][+-]?[0-9]+\\b)|       # .1E+3\n  (?:\\b[0-9]+[eE][+-]?[0-9]+\\b)|            # 1E+3\n  (?:\\b[0-9]+(\\.)[0-9]+\\b)|                # 1.1\n  (?:\\b[0-9]+(\\.)\\B)|                      # 1.\n  (?:\\B(\\.)[0-9]+\\b)|                      # .1\n  (?:\\b[0-9]+\\b(?!\\.))                     # 1\n)[L]?[fF]?","captures":{"0":{"name":"constant.numeric.decimal.fstar"},"1":{"name":"meta.delimiter.decimal.period.fstar"},"2":{"name":"meta.delimiter.decimal.period.fstar"},"3":{"name":"meta.delimiter.decimal.period.fstar"},"4":{"name":"meta.delimiter.decimal.period.fstar"},"5":{"name":"meta.delimiter.decimal.period.fstar"},"6":{"name":"meta.delimiter.decimal.period.fstar"}}},{"begin":"([(])\\s*(requires|ensures|decreases)?","end":"([)])","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"punctuation.definition.scope.begin.bracket.round.fstar"},"2":{"name":"keyword.other.fstar"}},"endCaptures":{"1":{"name":"punctuation.definition.scope.end.bracket.round.fstar"}}},{"begin":"([(])","end":"([)])","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"punctuation.definition.clause.begin.bracket.round.fstar"}},"endCaptures":{"1":{"name":"punctuation.definition.clause.end.bracket.round.fstar"}}},{"begin":"([%]\\[)","end":"(\\])","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"constant.language.termorder.begin.fstar"}},"endCaptures":{"1":{"name":"constant.language.termorder.end.fstar"}}},{"begin":"(\\[[@])","end":"(\\])","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"storage.modifier.attributes.begin.fstar"}},"endCaptures":{"1":{"name":"storage.modifier.attributes.end.fstar"}}},{"begin":"\\b(match)\\b","end":"\\b(with)\\b","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"keyword.control.match.fstar"}},"endCaptures":{"1":{"name":"keyword.control.with.fstar"}}},{"begin":"\\b(begin)\\b","end":"\\b(end)\\b","patterns":[{"include":"#expr"}],"beginCaptures":{"1":{"name":"keyword.control.begin.fstar"}},"endCaptures":{"1":{"name":"keyword.control.end.fstar"}}},{"match":"\\b([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\b(?!\\s*[.])","captures":{"1":{"name":"support.function.constructor.fstar"}}},{"match":"\\b((?:[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*[.])+)","captures":{"1":{"name":"variable.other.module.fstar"}}},{"match":"\\b([\\p{Ll}_][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)","captures":{"1":{"name":"entity.name.function.fstar"}}}]},"modules":{"patterns":[{"begin":"\\b(module)\\s+([\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)\\s*(=)","end":"\\b((?\u003cname\u003e[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g\u003cname\u003e)*)\\b","beginCaptures":{"1":{"name":"keyword.control.module.fstar"},"2":{"name":"variable.other.module-alias.fstar"},"3":{"name":"keyword.operator.assignment.fstar"}},"endCaptures":{"1":{"name":"variable.other.module.fstar"}}},{"begin":"\\b(module|open|include)\\b","end":"\\b((?\u003cname\u003e[\\p{Lu}\\p{Lt}][\\p{Lu}\\p{Lt}\\p{Ll}\\p{Lo}\\p{Lm}\\d'_]*)(?:[.]\\g\u003cname\u003e)*)\\b","beginCaptures":{"1":{"name":"keyword.control.module.fstar"}},"endCaptures":{"1":{"name":"variable.other.module.fstar"}}}]},"op_names":{"patterns":[{"name":"entity.name.tag.fstar","match":"\\bop(?:_(?:Multiply|Star|Slash|Percent|Plus|Substraction|Equals|Less|Greater|Bang|Dollar|Amp|Dot|Hat|Colon|Pipe|Question))+\\b"}]},"options":{"patterns":[{"match":"(#(?:re)?set-options)\\s*([\"])((?:[^\"]|\\\\\")*)([\"])","captures":{"1":{"name":"keyword.control.setoption.fstar"},"2":{"name":"punctuation.definition.options.begin.fstar"},"3":{"name":"string.quoted.double.fstar"},"4":{"name":"punctuation.definition.options.end.fstar"}}}]},"string_escapes":{"patterns":[{"name":"invalid.illegal.unicode-escape.fstar","match":"\\\\u(?![A-Fa-f0-9]{4}|{[A-Fa-f0-9]+})[^'\"]*"},{"name":"constant.character.escape.js","match":"\\\\u(?:[A-Fa-f0-9]{4}|({)([A-Fa-f0-9]+)(}))","captures":{"1":{"name":"punctuation.definition.unicode-escape.begin.bracket.curly.fstar"},"2":{"patterns":[{"name":"invalid.illegal.unicode-escape.fstar","match":"[A-Fa-f\\d]{7,}|(?!10)[A-Fa-f\\d]{6}"}]},"3":{"name":"punctuation.definition.unicode-escape.end.bracket.curly.fstar"}}},{"name":"constant.character.escape.fstar","match":"\\\\(x[0-9A-Fa-f]{2}|[0-2][0-7]{0,2}|3[0-6][0-7]?|37[0-7]?|[4-7][0-7]?|.)"}]},"strings":{"patterns":[{"name":"string.quoted.double.fstar","begin":"\"","end":"\"","patterns":[{"include":"#string_escapes"}],"beginCaptures":{"0":{"name":"punctuation.definition.string.begin.fstar"}},"endCaptures":{"0":{"name":"punctuation.definition.string.end.fstar"}}},{"name":"string.quoted.single.fstar","begin":"'","end":"'","patterns":[{"include":"#string_escapes"},{"name":"invalid.illegal.string.js","match":".{2,}"}],"beginCaptures":{"0":{"name":"punctuation.definition.char.begin.fstar"}},"endCaptures":{"0":{"name":"punctuation.definition.char.end.fstar"}}},{"name":"string.quoted.template.fstar","begin":"`","end":"`","patterns":[{"include":"#op_names"}],"beginCaptures":{"0":{"name":"punctuation.definition.operator.begin.fstar"}},"endCaptures":{"0":{"name":"punctuation.definition.operator.end.fstar"}}}]}}}