On Wed, Jan 22, 2020 at 10:51 AM Olivier Binda <[email protected]> wrote:
> 5) Mm0 > a) get a file for set.mm0 (set.mm translated to mm0) Mario, I'm looking > at you... > b) parse set.mm0 > c) extract a list of all mm0 ids > d) write a parser for mm0 statements > e) make the mephistolus Statement able to be build on mm0 stuff > I can send you the translated set.mm0 file (or you can run mm0-hs yourself to perform the translation), but I don't think it is necessarily representative of the things you will normally find in an MM0 file. It has no "def"s, for example, because set.mm uses axioms for definitions and the translator doesn't yet know enough to derive the equivalent def statement. A more representative sample is peano.mm0. If you want to parse theorems in set.mm, then the simplest way to get these is to read set.mm rather than translating it first. There are also tools for reading an MM0 file and turning it into an .mmu file, which has all statements and proofs written as s-expressions. This is probably much easier to parse, although it can get a bit big. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt4ngKXp4ihNcYbfw6j1hvCXajVr%3DA%2BBv-oGO8rs-R2DQ%40mail.gmail.com.
