4 files changed, 239 insertions, 0 deletions
diff --git a/runtime/queries/lean/folds.scm b/runtime/queries/lean/folds.scm
new file mode 100644
index 00000000..2c2bbb33
--- /dev/null
+++ b/runtime/queries/lean/folds.scm
@@ -0,0 +1,15 @@
+[
+  (namespace)
+  (section)
+
+  (instance)
+  (def)
+  (theorem)
+  (example)
+
+  (product)
+  (array)
+  (list)
+
+  (string)
+] @fold
diff --git a/runtime/queries/lean/highlights.scm b/runtime/queries/lean/highlights.scm
new file mode 100644
index 00000000..a64feb1d
--- /dev/null
+++ b/runtime/queries/lean/highlights.scm
@@ -0,0 +1,217 @@
+(open
+  namespace: (identifier) @namespace)
+(namespace
+  name: (identifier) @namespace)
+(section
+  name: (identifier) @namespace)
+
+;; Identifier naming conventions
+((identifier) @type
+ (#match? @type "^[A-Z]"))
+
+(arrow) @type
+(product) @type
+
+;; Declarations
+
+[
+  "abbrev"
+  "def"
+  "theorem"
+  "constant"
+  "instance"
+  "axiom"
+  "example"
+  "inductive"
+  "structure"
+  "class"
+
+  "deriving"
+
+  "section"
+  "namespace"
+] @keyword
+
+(attributes
+  (identifier) @function)
+
+(abbrev
+  name: (identifier) @type)
+(def
+  name: (identifier) @function)
+(theorem
+  name: (identifier) @function)
+(constant
+  name: (identifier) @type)
+(instance
+  name: (identifier) @function)
+(instance
+  type: (identifier) @type)
+(axiom
+  name: (identifier) @function)
+(structure
+  name: (identifier) @type)
+(structure
+  extends: (identifier) @type)
+
+(where_decl
+  type: (identifier) @type)
+
+(proj
+  name: (identifier) @field)
+
+(binders
+  type: (identifier) @type)
+
+["if" "then" "else"] @keyword.control.conditional
+
+["for" "in" "do"] @keyword.control.repeat
+
+(import) @include
+
+; Tokens
+
+[
+  "!"
+  "$"
+  "%"
+  "&&"
+  "*"
+  "*>"
+  "+"
+  "++"
+  "-"
+  "/"
+  "::"
+  ":="
+  "<"
+  "<$>"
+  "<*"
+  "<*>"
+  "<="
+  "<|"
+  "<|>"
+  "="
+  "=="
+  "=>"
+  ">"
+  ">"
+  ">="
+  ">>"
+  ">>="
+  "@"
+  "^"
+  "|>"
+  "|>."
+  "||"
+  "←"
+  "→"
+  "↔"
+  "∘"
+  "∧"
+  "∨"
+  "≠"
+  "≤"
+  "≥"
+] @operator
+
+[
+  "@&"
+] @operator
+
+[
+  "attribute"
+  "by"
+  "end"
+  "export"
+  "extends"
+  "fun"
+  "let"
+  "have"
+  "match"
+  "open"
+  "return"
+  "universe"
+  "variable"
+  "where"
+  "with"
+  "λ"
+  (hash_command)
+  (prelude)
+  (sorry)
+] @keyword
+
+[
+  "prefix"
+  "infix"
+  "infixl"
+  "infixr"
+  "postfix"
+  "notation"
+  "macro_rules"
+  "syntax"
+  "elab"
+  "builtin_initialize"
+] @keyword
+
+[
+  "noncomputable"
+  "partial"
+  "private"
+  "protected"
+  "unsafe"
+] @keyword
+
+[
+  "apply"
+  "exact"
+  "rewrite"
+  "rw"
+  "simp"
+  (trivial)
+] @keyword
+
+[
+  "catch"
+  "finally"
+  "try"
+] @exception
+
+((apply
+  name: (identifier) @exception)
+ (#match? @exception "throw"))
+
+[
+  "unless"
+  "mut"
+] @keyword
+
+[(true) (false)] @boolean
+
+(number) @constant.numeric.integer
+(float) @constant.numeric.float
+
+(comment) @comment
+(char) @character
+(string) @string
+(interpolated_string) @string
+; (escape_sequence) @string.escape
+
+; Reset highlighing in string interpolation
+(interpolation) @none
+
+(interpolation
+  "{" @punctuation.special
+  "}" @punctuation.special)
+
+["(" ")" "[" "]" "{" "}" "⟨" "⟩"] @punctuation.bracket
+
+["|" "," "." ":" ";"] @punctuation.delimiter
+
+(sorry) @error
+
+;; Error
+(ERROR) @error
+
+; Variables
+(identifier) @variable
diff --git a/runtime/queries/lean/injections.scm b/runtime/queries/lean/injections.scm
new file mode 100644
index 00000000..030714f1
--- /dev/null
+++ b/runtime/queries/lean/injections.scm
@@ -0,0 +1,2 @@
+((comment) @injection.content
+ (#set! injection.language "markdown"))
diff --git a/runtime/queries/lean/locals.scm b/runtime/queries/lean/locals.scm
new file mode 100644
index 00000000..dd6c2036
--- /dev/null
+++ b/runtime/queries/lean/locals.scm
@@ -0,0 +1,5 @@
+[
+  (module)
+  (namespace)
+  (section)
+] @local.scope