It is not hardcoded in mmj2, although it might be in the blacklist (which gets out of date relatively quickly anyway and knows how to handle it).
Regarding the naming, I think it is a bit odd that a theorem called a1ii does not use ax-1. Then again, idi doesn't use id either. On Tue, Nov 10, 2020 at 6:31 PM Scott Fenton <[email protected]> wrote: > Likewise for me and nf.mm > > On Nov 10, 2020, at 6:29 PM, Jim Kingdon <[email protected]> wrote: > > My answer is that iset.mm should do whatever set.mm does > > On November 10, 2020 2:51:35 PM PST, Benoit <[email protected]> > wrote: >> >> Hi all, >> >> I would like to relabel ~dummylink to ~a1ii, since it is the inference >> associated with ~a1i (and "dummylink" is not the prettiest word). >> >> As Norm told me, this might have a few consequences, so I would need some >> agreements before carrying on with the change: >> * I would propagate this change to iset.mm and nf.mm, so I'd like to >> have Jim Kingdon's and Scott Fenton's approvals. >> * The term "dummylink" is hard-coded in eimm.c, so it would have to be >> changed (easy). >> * Is it hard-coded in mmj2 ? >> * Is it used anywhere else ? >> >> Depending on the answers, it may or may not be too much trouble for such >> a small change. >> >> Thanks, >> Benoit >> >> -- > 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/6390F507-8FDB-4390-ADC2-469F5FA54831%40panix.com > <https://groups.google.com/d/msgid/metamath/6390F507-8FDB-4390-ADC2-469F5FA54831%40panix.com?utm_medium=email&utm_source=footer> > . > > -- > 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/A97F0E3A-CCC5-4C77-9265-136E9E209EA6%40gmail.com > <https://groups.google.com/d/msgid/metamath/A97F0E3A-CCC5-4C77-9265-136E9E209EA6%40gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs9ySUgH-09GaFj5PZxXx-YHNF%2BSw79dQ6m0JeYRJZqug%40mail.gmail.com.
