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?
I think our tradition has been to use ALT for alternate proofs, so not overwriting the proof with the non-ALT version is undesirable. Should we even be using ALT for variations of theorems as opposed to alternate proofs? What is the purpose of having a modified theorem in set.mm if it isn't intended to be used? Or it if is intended to be used, perhaps a different theorem name like dfss2, dfss3,... Of course the ALT proof can still be minimized with overrides, after someone analyzes the purpose of the ALT in each case. Perhaps we should consider the ALT suffix as meaning "avoid" and "needs special handling" in which case both discouragements would be appropriate in general. Norm On Tuesday, February 25, 2020 at 12:28:15 PM UTC-5, Alexander van der Vekens wrote: > > To check that both tags are provided for *OLD statements is OK. > > I would feel not comfortable, however, if all ALT theorems/definitions > must have both tags. "(New usage is discouraged.)" would be OK, but not > "(Proof modification is discouraged.)". I think we have two meanings of > ALT: alternate proofs or alternate definitions/variants of theorems. For > the first case "(Proof modification is discouraged.)" makes sense, but not > for the second case: here I would like to have shorter proofs (found > automatically) if possible. A solution could be to provide two separate > suffixes: ALTP for "alternate proof", ALT for "alternate > definitions/variants of theorems". > -- 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/5583476b-7f1d-492e-9213-2647b80d1ecd%40googlegroups.com.
