message: Highlight characters like strings.
  This is consistent with the C++ highlighting.
diff: ]
  },
  { "name": "constant.language.lean4", "match": "\\b(true|false)\\b" },
  - { "name": "constant.character.lean4", "match": "'[^\\\\']'" },
  - { "name": "constant.character.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": "'[^\\\\']'" },
  + { "name": "string.quoted.single.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]|.))'",
  "captures": { "1": { "name": "constant.character.escape.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" }
  