const lang = Object.freeze(JSON.parse("{\"displayName\":\"Lean 4\",\"fileTypes\":[],\"name\":\"lean\",\"patterns\":[{\"include\":\"#comments\"},{\"match\":\"\\\\b(Prop|Type|Sort)\\\\b\",\"name\":\"storage.type.lean4\"},{\"match\":\"\\\\battribute\\\\b\\\\s*\\\\[[^]]*]\",\"name\":\"storage.modifier.lean4\"},{\"match\":\"@\\\\[[^]]*]\",\"name\":\"storage.modifier.lean4\"},{\"match\":\"\\\\b(?<!\\\\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\\\\.)\\\\b\",\"name\":\"storage.modifier.lean4\"},{\"match\":\"\\\\b(sorry|admit|stop)\\\\b\",\"name\":\"invalid.illegal.lean4\"},{\"match\":\"#(print|eval|reduce|check|check_failure)\\\\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|constant)\\\\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|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universes??|variables??|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infixl??|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\\\\.)\\\\b\",\"name\":\"keyword.other.lean4\"},{\"begin\":\"«\",\"contentName\":\"entity.name.lean4\",\"end\":\"»\"},{\"begin\":\"(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\":\"'[^'\\\\\\\\]'\",\"name\":\"string.quoted.single.lean4\"},{\"captures\":{\"1\":{\"name\":\"constant.character.escape.lean4\"}},\"match\":\"'(\\\\\\\\(x\\\\h\\\\h|u\\\\h\\\\h\\\\h\\\\h|.))'\",\"name\":\"string.quoted.single.lean4\"},{\"match\":\"`+[^(\\\\[]\\\\S+\",\"name\":\"entity.name.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\",\"aliases\":[\"lean4\"]}"))

export default [
lang
]