Created
October 26, 2020 14:25
-
-
Save lildude/8a44881b037673c42ad4f18253d30859 to your computer and use it in GitHub Desktop.
Testing Lean grammars
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "name": "Lean", | |
| "scopeName": "source.lean", | |
| "patterns": [ | |
| { | |
| "include": "#comments" | |
| }, | |
| { | |
| "name": "meta.definitioncommand.lean", | |
| "begin": "\\b(?\u003c!\\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\\b\\s+(\\{[^}]*\\})?", | |
| "end": "(?=\\bwith\\b|\\bextends\\b|[:\\|\\(\\[\\{⦃\u003c\u003e])", | |
| "patterns": [ | |
| { | |
| "include": "#comments" | |
| }, | |
| { | |
| "include": "#definitionName" | |
| }, | |
| { | |
| "match": "," | |
| } | |
| ], | |
| "beginCaptures": { | |
| "1": { | |
| "name": "keyword.other.definitioncommand.lean" | |
| } | |
| } | |
| }, | |
| { | |
| "name": "storage.type.lean", | |
| "match": "\\b(Prop|Type|Sort)\\b" | |
| }, | |
| { | |
| "name": "storage.modifier.lean", | |
| "match": "\\battribute\\b\\s*\\[[^\\]]*\\]" | |
| }, | |
| { | |
| "name": "storage.modifier.lean", | |
| "match": "@\\[[^\\]]*\\]" | |
| }, | |
| { | |
| "name": "keyword.control.definition.modifier.lean", | |
| "match": "\\b(?\u003c!\\.)(private|meta|mutual|protected|noncomputable)\\b" | |
| }, | |
| { | |
| "name": "invalid.illegal.lean", | |
| "match": "\\b(sorry)\\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|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\\.)\\b" | |
| }, | |
| { | |
| "name": "keyword.other.lean", | |
| "match": "\\b(?\u003c!\\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\\.)\\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": "`+[^\\[(]\\S+" | |
| }, | |
| { | |
| "name": "constant.numeric.lean", | |
| "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+))\\b" | |
| } | |
| ], | |
| "repository": { | |
| "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": "\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*" | |
| }, | |
| { | |
| "contentName": "entity.name.function.lean", | |
| "begin": "«", | |
| "end": "»" | |
| } | |
| ] | |
| }, | |
| "docComment": { | |
| "name": "comment.block.documentation.lean", | |
| "begin": "/--", | |
| "end": "-/", | |
| "patterns": [ | |
| { | |
| "include": "source.lean.markdown" | |
| }, | |
| { | |
| "include": "#blockComment" | |
| } | |
| ] | |
| }, | |
| "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" | |
| } | |
| ] | |
| } | |
| } | |
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "name": "Lean", | |
| "scopeName": "source.lean", | |
| "patterns": [ | |
| { | |
| "include": "#dashComment" | |
| }, | |
| { | |
| "include": "#blockComment" | |
| }, | |
| { | |
| "name": "meta.import.lean", | |
| "begin": "^\\s*(import)\\b", | |
| "end": "$", | |
| "beginCaptures": { | |
| "1": { | |
| "name": "keyword.other.lean" | |
| } | |
| } | |
| }, | |
| { | |
| "name": "meta.names.lean", | |
| "begin": "\\b(inductive|structure|record|theorem|proposition|axiom|axioms|lemma|hypothesis|definition|def|instance|class|constant)\\b[ \\t\\n\\r({\\[]+([^ \\t\\n\\r{(\\[]*)", | |
| "end": "[ \\t\\n\\r{(\\[]", | |
| "beginCaptures": { | |
| "1": { | |
| "name": "keyword.other.lean" | |
| }, | |
| "2": { | |
| "name": "variable.language.lean" | |
| } | |
| } | |
| }, | |
| { | |
| "name": "string.quoted.double.lean", | |
| "begin": "\"", | |
| "end": "\"", | |
| "patterns": [ | |
| { | |
| "name": "constant.character.escape.lean", | |
| "match": "\\\\." | |
| } | |
| ] | |
| }, | |
| { | |
| "name": "storage.type.lean", | |
| "match": "\\b(Prop|Type[\\'₊₀-₉]?)" | |
| }, | |
| { | |
| "name": "storage.modifier.lean", | |
| "match": "@\\[[^\\]]*\\]" | |
| }, | |
| { | |
| "name": "storage.modifier.lean", | |
| "match": "attribute\\s*\\[[^\\]]*\\]" | |
| }, | |
| { | |
| "name": "keyword.other.lean", | |
| "match": "\\b(import|prelude|theory|protected|private|noncomputable|mutual|meta|definition|def|instance|renaming|hiding|exposing|parameter|parameters|begin|conjecture|constant|constants|hypothesis|lemma|corollary|variable|variables|premise|premises|print|theorem|example|abbreviation|context|open|as|export|axiom|inductive|with|structure|record|universe|universes|alias|help|override|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|vm_eval|eval|check|exit|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|metaclasses|raw|run_command)\\b" | |
| }, | |
| { | |
| "name": "keyword.other.lean", | |
| "match": "\\b(calc|have|assert|suppose|this|match|obtains|do|suffices|show|by|in|at|let|forall|fun|exists|if|then|else|assume|take|obtain|from)\\b" | |
| }, | |
| { | |
| "name": "constant.language.lua", | |
| "match": "(-\u003e|==|:=|\u003c-\u003e|\\\\/|/\\\\|\u003c=|\u003e=|⁻¹)" | |
| }, | |
| { | |
| "name": "constant.language.lua", | |
| "match": "[#@∼↔/=∧∨≠\u003c\u003e≤≥¬⬝▸+*-]" | |
| }, | |
| { | |
| "name": "keyword.operator.lean", | |
| "match": "(?\u003c=\\s)[=→λ∀?]" | |
| }, | |
| { | |
| "name": "string.quoted.double.lean", | |
| "begin": "\"", | |
| "end": "\"", | |
| "patterns": [ | |
| { | |
| "name": "constant.character.escape.lean", | |
| "match": "\\\\(NUL|SOH|STX|ETX|EOT|ENQ|ACK|BEL|BS|HT|LF|VT|FF|CR|SO|SI|DLE|DC1|DC2|DC3|DC4|NAK|SYN|ETB|CAN|EM|SUB|ESC|FS|GS|RS|US|SP|DEL|[abfnrtv\\\\\\\"'\\\u0026])" | |
| }, | |
| { | |
| "name": "constant.character.escape.octal.lean", | |
| "match": "\\\\o[0-7]+|\\\\x[0-9A-Fa-f]+|\\\\[0-9]+" | |
| }, | |
| { | |
| "name": "constant.character.escape.control.lean", | |
| "match": "\\^[A-Z@\\[\\]\\\\\\^_]" | |
| } | |
| ], | |
| "beginCaptures": { | |
| "0": { | |
| "name": "punctuation.definition.string.begin.lean" | |
| } | |
| }, | |
| "endCaptures": { | |
| "0": { | |
| "name": "punctuation.definition.string.end.lean" | |
| } | |
| } | |
| }, | |
| { | |
| "name": "constant.numeric.lean", | |
| "match": "\\b([0-9]+|0([xX][0-9a-fA-F]+))\\b" | |
| } | |
| ], | |
| "repository": { | |
| "blockComment": { | |
| "name": "comment.block.lean", | |
| "begin": "/-", | |
| "end": "-/", | |
| "captures": { | |
| "0": { | |
| "name": "punctuation.definition.comment.lean" | |
| } | |
| } | |
| }, | |
| "dashComment": { | |
| "name": "comment.line.double-dash.lean", | |
| "begin": "(--)", | |
| "end": "$", | |
| "beginCaptures": { | |
| "0": { | |
| "name": "punctuation.definition.comment.lean" | |
| } | |
| } | |
| }, | |
| "identifier": { | |
| "name": "entity.name.function.lean", | |
| "match": "\\b[^\\(\\)\\{\\}[:space:]=→λ∀?][^\\(\\)\\{\\}[:space:]]*" | |
| } | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment