I found proof decompression to be easier to implement than I thought it would be. The hardest part was just understanding how it works.
On Tuesday, December 3, 2019 at 3:32:07 PM UTC+1, 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 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/c40d837c-6e17-4030-93c7-d72b35e817f5%40googlegroups.com.
