What's most impressive about it is that it uses a system, Megaladon, which is pretty obscure. There isn't that much documentation or examples, but it can still formalize an advanced undergraduate textbook.