I also wonder whether this would be better expressed as a $j comment rather than another plain text comment in the doc string. It's not really important user-facing information.
On Sun, Jul 17, 2022 at 12:57 PM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/d1f0a889-7d14-4e56-95d9-acef10ba8102n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs2%3DHRRoPTJdM5LkVK%2BRJbYtAdncnsPJ%2BQG%2BP-%3DYhiL%3Dw%40mail.gmail.com.
