{
  "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": "#blockComment"
        }
      ]
    },
    "comments": {
      "patterns": [
        {
          "include": "#dashComment"
        },
        {
          "include": "#docComment"
        },
        {
          "include": "#modDocComment"
        },
        {
          "include": "#blockComment"
        }
      ]
    },
    "dashComment": {
      "name": "comment.line.double-dash.lean",
      "begin": "(--)",
      "end": "$",
      "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"
        }
      ]
    }
  }
}