On Sunday, July 17, 2022 at 6:36:13 PM UTC+2 David A. Wheeler wrote: > I propose using these comment markings for assertions ($a and $p) where > hypotheses > are not used on *purpose*: > * "(Intentionally unused hypothesis)" if exactly one hypothesis is unused > * "(Intentionally unused hypotheses)" if more than one hypotheses are > unused > > I was originally going to propose both simply because that's how English > plurals work. > However, there's an error-detect advantage to making their meaning > different - > if you only intended 1 hypothesis to be unused, but more than one is, it > can still be caught. > This is a good idea, especially if there is a tool/script which checks automatically if there are (unintentionally) unused hypotheses. But from this tool perspective, I would suggest to have only one marking:
* "(Intentionally unused hypotheses)" if at least one hypothesis is unused It is the responsibility of the contributor who uses such a marking that the hypotheses are as intended - the tool/script can check all other cases, which will be the vast majority. -- 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/d1f0a889-7d14-4e56-95d9-acef10ba8102n%40googlegroups.com.
