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/b539f3d1-1069-45a6-a174-352b19361302n%40googlegroups.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/6390F507-8FDB-4390-ADC2-469F5FA54831%40panix.com.
