I think it's overkill for something that basically never happens. Are there cases in set.mm apart from a1ii (which is said to be useful for use in some proof assistants, but I don't even know if it's ever used) and bj-df-clel, bj-df-cleq (which are candidates to replace df-clel, df-cleq, in which case they will become $a-statements anyway) ? Benoît
On Sunday, July 17, 2022 at 7:01:18 PM UTC+2 [email protected] wrote: > 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/3c546ae4-c8da-4bc0-96d5-9727b9039690n%40googlegroups.com.
