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/b539f3d1-1069-45a6-a174-352b19361302n%40googlegroups.com.
