Metamath is a formal language to express mathematical theorems and
proofs developed by Norman Megill. [1, 2]
The language is defined in the documentation [3, Chapter 4]. The syntax
highlighter is a bit lenient sometimes. When encountering symbols, we
highlight them as variables, because only semantic analysis could tell
if they are symbols instead.
The test is a modified version of the file demo0.mm in [4], where I
removed most of the comments.
I'm not sure if we should set a priority, because apparently Objective-
C++ files have the same extension. Right now it is a toss-up between the
two languages.
[1] http://us.metamath.org/
[2] https://en.wikipedia.org/wiki/Metamath
[3] http://us.metamath.org/downloads/metamath.pdf
[4] http://us.metamath.org/downloads/metamath.tar.bz2