set.mm in metamath zero

Stream: general

[Huỳnh Trần Khanh]

hmm so metamath has a very big set.mm file but I find metamath zero much easier to understand and it also has better vscode integration... can I open set.mm in metamath zero? is there a ported version somewhere

[Mario Carneiro]

It is possible to port set.mm to MM0, but the result is not particularly good for reading: notations are (mostly) lost, and comments are not preserved either. The best way to read metamath is to use the web pages like http://us.metamath.org/mpeuni/ru.html , or use the metamath program which has a command line interface to search theorems or present proofs in various forms.

[Mario Carneiro]

That is, metamath is not optimized for reading from source, and relies more heavily on tool support for interpretation than most other languages you might be familiar with