{"name":"Lean","scopeName":"source.lean","patterns":[{"include":"#comments"},{"name":"meta.definitioncommand.lean","begin":"\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|abbreviation|lemma|definition|def|class)\\b\\s+((\\{)([^}]*)(\\}))?","end":"(?=\\bwith\\b|\\bextends\\b|:|\\||\\.|\\(|\\[|\\{|⦃)","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean"},"2":{"name":"meta.binder.universe.lean"},"3":{"name":"punctuation.definition.binder.universe.begin.lean"},"4":{"name":"variable.other.constant.universe.lean"},"5":{"name":"punctuation.definition.binder.universe.end.lean"}}},{"name":"meta.definitioncommand.lean","begin":"\\b(?\u003c!\\.)(example|instance)\\b\\s+","end":"(?=:|\\||\\.|\\(|\\[|\\{|⦃)","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean"}}},{"name":"meta.definitioncommand.lean","begin":"\\b(?\u003c!\\.)(axiom|axioms|constant)\\b\\s+(\\{[^}]*\\})?","end":"($|(?=:|\\||\\.|\\(|\\[|\\{|⦃))","patterns":[{"include":"#comments"},{"include":"#definitionName"},{"match":","}],"beginCaptures":{"1":{"name":"keyword.other.definitioncommand.lean"}}},{"name":"storage.modifier.lean","begin":"\\battribute\\b\\s*\\[","end":"\\]","patterns":[{"include":"#expressions"}]},{"name":"storage.modifier.lean","begin":"@\\[","end":"\\]","patterns":[{"include":"#expressions"}]},{"name":"keyword.control.definition.modifier.lean","match":"\\b(?\u003c!\\.)(private|meta|mutual|protected|noncomputable)\\b"},{"name":"keyword.other.command.lean","match":"#print\\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\\b"},{"name":"keyword.other.command.lean","match":"#(print|eval|reduce|check|help|exit|find|where)\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|constant|lemma|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\\.)\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(variable|variables|parameter|parameters|constants)(?!\\.)\\b"},{"include":"#expressions"}],"repository":{"binderName":{"patterns":[{"name":"variable.parameter.lean","match":"(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ])*"},{"contentName":"variable.parameter.lean","begin":"«","end":"»"}]},"blockComment":{"name":"comment.block.lean","begin":"/-","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"comments":{"patterns":[{"include":"#dashComment"},{"include":"#docComment"},{"include":"#stringBlock"},{"include":"#modDocComment"},{"include":"#blockComment"}]},"dashComment":{"name":"comment.line.double-dash.lean","begin":"(--)","end":"$","patterns":[{"include":"source.lean.markdown"}],"beginCaptures":{"0":{"name":"punctuation.definition.comment.lean"}}},"definitionName":{"patterns":[{"name":"entity.name.function.lean","match":"(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ])*(\\.(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ])*)*"},{"contentName":"entity.name.function.lean","begin":"«","end":"»"}]},"docComment":{"name":"comment.block.documentation.lean","begin":"/--","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"expressions":{"patterns":[{"name":"storage.type.lean","match":"\\b(Prop|Type|Sort)\\b"},{"name":"invalid.illegal.lean","match":"\\b(sorry)\\b"},{"contentName":"entity.name.lean","begin":"«","end":"»"},{"name":"keyword.control.lean","match":"\\b(?\u003c!\\.)(if|then|else)\\b"},{"name":"string.quoted.double.lean","begin":"\"","end":"\"","patterns":[{"name":"constant.character.escape.lean","match":"\\\\[\\\\\"nt']"},{"name":"constant.character.escape.lean","match":"\\\\x[0-9A-Fa-f][0-9A-Fa-f]"},{"name":"constant.character.escape.lean","match":"\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]"}],"beginCaptures":{"0":{"name":"punctuation.definition.string.begin.lean"}},"endCaptures":{"0":{"name":"punctuation.definition.string.end.lean"}}},{"name":"string.quoted.single.lean","match":"'[^\\\\']'"},{"name":"string.quoted.single.lean","match":"'(\\\\(x..|u....|.))'","captures":{"1":{"name":"constant.character.escape.lean"}}},{"name":"entity.name.lean","match":"`+(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ])*"},{"name":"constant.numeric.lean","match":"\\b([0-9]+|0([xX][0-9a-fA-F]+))\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(calc|have|this|match|do|suffices|show|by|in|at|let|from|obtain|haveI)(?!\\.)\\b"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)λ"},{"name":"keyword.other.lean","match":"\\b(?\u003c!\\.)(begin|end|using)(?!\\.)\\b"},{"name":"meta.parens","begin":"\\(","end":"\\)","patterns":[{"contentName":"meta.type.lean","begin":":","end":"(?=\\))","patterns":[{"include":"#expressions"}],"beginCaptures":{"0":{"name":"punctuation.separator.type.lean"}}},{"include":"#expressions"}]},{"include":"#dashComment"},{"include":"#blockComment"},{"include":"#stringBlock"}]},"modDocComment":{"name":"comment.block.documentation.lean","begin":"/-!","end":"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]},"stringBlock":{"name":"comment.block.string.lean","begin":"/-\"","end":"\"-/","patterns":[{"include":"source.lean.markdown"},{"include":"#blockComment"}]}}}