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.
-- 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.
