> On Jul 17, 2022, at 1:42 PM, Mario Carneiro <[email protected]> wrote:
>
> 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.
A "$j" works for me, I just want theorems with intentionally-unused hypotheses
marked in a way that automated tools *can* detect it. It should be very rare.
-- David A. Wheeler
--
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/9834631B-2DDF-4E7D-8F12-15703FA826C1%40dwheeler.com.
