Hell, Thanks for the quick turnaround. > The book looks like a related project to metamath, like advanced > documentation, not like a regular manual. I didn't read it, so it is > just a guess. Oh, okay. That makes sense. PDF as official documentation is certainly strange for what looks like a cli program. In this case, it just happens that this is the only reasonable documentation, aparth from the website, for using and understanding Metamath proofs. > I do. In any case, if you want to keep them, they need to start with two > semicolons, not a single one. > > WDYT? I trust your initial impression on this one. Let's use the patch from my previous email that excises the commented out code. Does it look reasonable? Cheers.