On Tuesday, February 25, 2020 at 9:02:25 PM UTC+1, Norman Megill wrote: > > 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? > Yes, I fully agree!
> 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. > Also OK for me. -- 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/85b7032a-7cbc-4911-a7de-c2f02202774a%40googlegroups.com.
