On Sun, 12 Jan 2020 16:09:16 -0800 (PST), Norman Megill <[email protected]> wrote: > I don't think it's necessarily because both of these will automatically be > removed with 'minimize'. ...
Okay, how about marking just idi with "(New usage is discouraged.)"? I *do* refer to idi in a tutorial, and it's useful in some cases, I just don't want it to be automatically matched. Details below. --- David A. Wheeler ========= DETAILS ========================= This is really about mmj2. I'm trying to update the mmj2 tutorial. I found that you start up mmj2 with this: h1::reiteration.1 |- ph qed:1: |- ph A control-U will automatically prove that using idi: h1::reiteration.1 |- ph qed:1:idi |- ph $= ( reiteration.1 idi ) ABC $. I think we want to avoid automatic use of dummylink and idi; someone should specifically *request* it (by referring to its reference). > 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. I specifically mentioned in my tutorial using idi to copy a statement so it can then be edited. So there's a *use* for it, I just don't want it used unintentionally. > 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. Ok, I didn't realize that was a nuisance. Never mind. Can we just mark idi as "(New usage is discouraged.)" then? I presume we don't want people to use it unless they *mean* to use it, and your use only uses dummylink. mmj2 already has a RunParms which prevents use of dummylink. It currently says: ProofAsstUnifySearchExclude,biigb,xxxid,dummylink I think I can bring it all the way down to *just* dummylink. The first was renamed biigb -> dfbi1gb -> dfbi1ALT whose use is discouraged anyway, and xxxid doesn't exist any more. For the rest we're using the "New usage is discouraged", which is easier to maintain anyway. -- 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/E1iqp82-000385-SA%40rmmprod07.runbox.
