Zulip Chat Archive

Stream: general

Topic: set.mm in metamath zero

Huỳnh Trần Khanh (Dec 27 2021 at 03:49):

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 (Dec 27 2021 at 04:57):

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 (Dec 27 2021 at 04:57):

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

Last updated: Dec 20 2023 at 11:08 UTC