> On Jul 17, 2022, at 1:01 PM, Mario Carneiro <[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.
Maybe. I think it *is* useful for users to know that at least one of they
hypotheses they see isn't really necessary, and it doesn't really impact the
mathematical interpretation of the assertion. Obviously it would *work* either
way. I'm curious what other think.
BTW, if we just a comment marking, it should have a full stop before the
closing parenthesis just like similar markings. That is:
* "(Intentionally unused hypotheses.)"
--- 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/AC73ECEF-EE9C-4363-A7E0-28EE7EA643CA%40dwheeler.com.
