Eric Hall
Eric Hall
Encountered the same issue. HOL munger would produce output which would be displayed in the PDF despite the relevant statement being inside a comment. Workaround: mangle the command so that...
That sounds good! I'll have to check it out next time I need to write a recursive function. Would be good to have it incorporated into the `Definition ... End`...
I, too, like to replace parts of my definition with ARB to ensure that the rest of the definition is being type-checked correctly, and then fill in the ARBs later....