I don't think it's necessarily because both of these will automatically be removed with 'minimize'.
While I may be the only one to do so, I have used dummylink to build proofs in MM-PA to work around the "backwards only" method it requires. Making it 'discouraged' will be a nuisance that I'll have to override. dummylink is also used by the eimm program (see Metamath Home Page) to import partial mmj2 proofs into MM-PA. 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. Norm On Sunday, January 12, 2020 at 6:25:15 PM UTC-5, David A. Wheeler wrote: > > I propose that dummylink & idi be marked with > "(New usage is discouraged.)". > > As noted in the text, > they should normally never appear in a completed proof. > Marking them this way will prevent them from being > automatically used, and I think that's usually what is wanted. > The normal mmj2 invocation has special case stuff to > avoid its invocation, but that was created before we > had the marking "(New usage is discouraged.)". > Of course, someone can specifically *force* its use, but > then it will noticed as such. > > I noticed this while trying to update the mmj2 tutorial. > > Does that seem reasonable? > > --- 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/90f05118-acbc-44eb-bb36-ef5b72fe8406%40googlegroups.com.
