In: https://github.com/metamath/set.mm/issues/2648 @savask reveals some great analysis of theorems that don't use some of their hypotheses. In most cases this is something that should be fixed. It's great work, thanks!!
However, as @savask notes: > ... there are also theorems which contain useless hypotheses by design, like > a1ii, which shouldn't be corrected. I think every assertion that intentionally does *not* use all its hypotheses should be *clearly* documented in its descriptive comment. I think we should have a convention so we can automatically detect those cases later, similar to "(New usage is discouraged.)". That way, both humans and automated analysis programs will know that this is on purpose. 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. --- 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/C93E2B1C-03A7-420B-AD4D-CD1E9C843B66%40dwheeler.com.
