I think that if it's only going to appear once or a few times, I would rather have it as a $j comment than a markup keyword, since the latter is more likely to not be recognized as a keyword. (I am generally opposed to markup keywords altogether - I would rather have computer-readable keywords be explicitly called out as such and presentation tools should incorporate this in the e.g. HTML display if desired.) $j commands are also fairly low cost since they do not mandate the existence of any tool that recognizes them (there are a couple $j commands that are already in that category) - the only thing that is needed is to make up a keyword and write it in the file, and tools can decide to honor the annotation if they want to.
On Sun, Jul 17, 2022 at 1:12 PM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/3c546ae4-c8da-4bc0-96d5-9727b9039690n%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/CAFXXJSvcVev6%3DwKe%3Dt78OGm-Ow3ug%2BV5e6Jfg%2B3_biEShDcBMw%40mail.gmail.com.
