On Tuesday, February 25, 2020 at 1:40:54 PM UTC-5, Alexander van der Vekens wrote: > > On Tuesday, February 25, 2020 at 7:00:48 PM UTC+1, Norman Megill wrote: >> >> Since there were no other replies, unfortunately I just updated set.mm >> with both discouragements on every ALT because of the problems they were >> creating. I suppose I could revert and do the analysis all over, but I >> want to get the minimizations applied soon without unwanted side effects. >> How many of your theorems does this affect? >> > Sorry, I was on a journey over the weekend... > But don't worry, there are some ALT definitions/theorems in my mathbox > about magmas/semigroups and graphs which are affected. For these, I can > take care by myself. So if we use ALT for alternate proofs only (in the > future), we could use Alt for "alternate definitions/variants of theorems". > Then we can check the tags for *ALT theorems, and will have no checks for > *Alt theorems. >
Not sure if "Alt" vs. "ALT" will be confusing; I was going to suggest ALTV for alternate version. But any suffix will do. What I propose is that the ALT suffix be treated as a kind of markup keyword that will always require both discouragements, regardless of what it is used for, and anything else like *Alt or *ALTV will be ignored by 'verify markup' i.e. treated as just another label so you can do anything you want with it as far as discouragements. Basically, then, *OLD and *ALT will be the only "keyword" patterns recognized by 'verify markup' for the time being and will require both discouragements. It might be useful to add more patterns in the future, but let's keep it simple for now. The essential difference between OLD and ALT is that OLD will expire and eventually be deleted. Agreed? Therefore I won't revert the discouragement commit, and at some point you can change the labels and discouragements in your mathbox per your preference. I'm not aware of any other such situations outside of your mathbox, but if there are any they can be handled individually as the need arises. Norm -- 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/9e26516f-f494-4548-9cd3-4234d57bb126%40googlegroups.com.
