Relabeling ~dummylink

[Benoit]

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

[Jim Kingdon]

My answer is that iset.mm should do whatever set.mm does

[Scott Fenton]

Likewise for me and nf.mm

On Nov 10, 2020, at 6:29 PM, Jim Kingdon <kin...@panix.com> wrote:

My answer is that iset.mm should do whatever set.mm does

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6390F507-8FDB-4390-ADC2-469F5FA54831%40panix.com.

[Mario Carneiro]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/A97F0E3A-CCC5-4C77-9265-136E9E209EA6%40gmail.com.