I agree; I think implementing compressed proof reading is worth the effort,
particularly because of the exponential speedup over uncompressed proofs
(in the worst case). The scheme is pretty simple to work with. Be sure to
read appendix C of the metamath book, which lays it all out clearly.
On
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
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
>
>
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
