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 

Reply via email to