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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com.