Uncompressing the entire set.mm database was last discussed here https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ
Can your verifier check demo0.mm yet? ( https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm) Best regards, Antony On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic <[email protected]> wrote: > Well, at any rate as I've been working on this for 9 days now I'll stop > here. I do not feel like going those last few extra miles just to implement > proof decompression and test it thoroughly on the big library. I am not > sure how stringent the criteria for inclusion on that list of verifiers in > other languages are, but it might be good enough for consideration anyway > even in its current form. > > I am impatient to start studying set theory so I'll get to that. That was > what attracted me to Metamath in the first place. Doing this toy > implementation was a side quest. > > -- > 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/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAJ48g%2BAJN4v1YnW%3DDxLB8dtLK_20%3DwgjBfXGcnhJHJ0_ro_rag%40mail.gmail.com.
