On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill <[email protected]> wrote: > > > Alan Sare's tool "completeusersproof" appears to make use of idi, at least > it appears in his C code and is referenced extensively in the program > comments. Although this program probably has a very small user base, I > think we should leave in idi and also not mark it discouraged so that > proofs generated by the code won't be rejected. Any idi usage in the > generated proofs will be removed by 'minimize'.
We could just ask people to use 'minimize' before submitting proofs generated by that tool. But if that's not convincing enough, that's fine. I couldn't think of a reason *not* to do this, but I didn't know about those other situations. You learn something every day!! If idi won't be marked like this, I'll probably propose to Mario that this RunParms.txt line: ProofAsstUnifySearchExclude,biigb,xxxid,dummylink be changed to: ProofAsstUnifySearchExclude,dummylink,idi I think that for mmj2 users it would have a similar effect. --- David A. Wheeler -- 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/E1iqpGZ-0003lI-5g%40rmmprod07.runbox.
