6 lines
4.6 KiB
JavaScript
6 lines
4.6 KiB
JavaScript
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|universe|universes|variable|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|infix|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\":\"\\\\\\\\[\\\\\\\\\\\"ntr']\",\"name\":\"constant.character.escape.lean4\"},{\"match\":\"\\\\\\\\x[0-9A-Fa-f][0-9A-Fa-f]\",\"name\":\"constant.character.escape.lean4\"},{\"match\":\"\\\\\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]\",\"name\":\"constant.character.escape.lean4\"}]},{\"begin\":\"\\\"\",\"end\":\"\\\"\",\"name\":\"string.quoted.double.lean4\",\"patterns\":[{\"match\":\"\\\\\\\\[\\\\\\\\\\\"ntr']\",\"name\":\"constant.character.escape.lean4\"},{\"match\":\"\\\\\\\\x[0-9A-Fa-f][0-9A-Fa-f]\",\"name\":\"constant.character.escape.lean4\"},{\"match\":\"\\\\\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]\",\"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[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'\",\"name\":\"string.quoted.single.lean4\"},{\"match\":\"`+[^\\\\[(]\\\\S+\",\"name\":\"entity.name.lean4\"},{\"match\":\"\\\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(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\":\"#stringBlock\"},{\"include\":\"#modDocComment\"},{\"include\":\"#blockComment\"}]},\"dashComment\":{\"begin\":\"--\",\"end\":\"$\",\"name\":\"comment.line.double-dash.lean4\",\"patterns\":[{\"include\":\"source.lean4.markdown\"}]},\"definitionName\":{\"patterns\":[{\"match\":\"\\\\b[^:«»\\\\(\\\\)\\\\{\\\\}[:space:]=→λ∀?][^:«»\\\\(\\\\)\\\\{\\\\}[:space:]]*\",\"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
|
|
]
|