Yeah, it works fine on demo0.mm. I did some examples by hand to make sure that disjointment constraints are verified properly as well.
Dana utorak, 3. prosinca 2019. u 16:18:22 UTC+1, korisnik Antony Bartlett napisao je: > > 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 <mra...@gmail.com > <javascript:>> 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 meta...@googlegroups.com <javascript:>. >> 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a299c546-ecc3-4020-a199-139d2c00a2a7%40googlegroups.com.