[Metamath] How to process dummylink?

I am working on my own verifier and am in the debugging stage. I can verify demo0.mm, but I've encountered a strange issue while trying to verify set.mm. *dummylink $p |- ph $=* * ( ) C $.* I am not sure what *C* is here, but *(* and *)*

[Metamath] Re: How to process dummylink?

Sorry about this, as soon as I posted I realized that I had completely forgotten about compressed proofs. -- 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+u

[Metamath] Re: How to process dummylink?

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

Re: [Metamath] Re: How to process dummylink?

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

Re: [Metamath] Re: How to process dummylink?

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 > > ht

Re: [Metamath] Re: How to process dummylink?

On Tue, 3 Dec 2019 06:32:07 -0800 (PST), Marko Grdinic 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