On Sunday, January 12, 2020 at 7:09:17 PM UTC-5, Norman Megill wrote: > > As for idi, I don't really care - mmj2 used to make use of it but I don't > think it does anymore. As far as I am concerned, we can delete idi unless > someone has a use for it. > > 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'.
My overall opinion then is that neither dummylink nor idi should be discouraged or deleted. Do you have any other reason for discouraging them? Norm -- 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/56fda8dd-2f70-48b1-95af-82a2deff4f3b%40googlegroups.com.
