Testing Lean grammars

v7.11.1-source.lean.json

{
  "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"
        }
      ]
    }
  }
}

v7.5.0-source.lean.json

{
  "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:]]*"
    }
  }
}