I fully agree with Benoit here, this almost never happens so adding a $j command or a special comment is just over-bureaucratization of set.mm.
I would also argue that an automatic check for unused hypotheses (like we do with markup) is not needed. It may happen that a proof of some statement uses all its hypotheses originally, but stops using some hypothesis after automatic minimization. This will trigger our hypothetical automatic check, and while minimization can be done automatically very easily, removing unused hypotheses requires work. This will impose additional toll on already not-so-easy process of contributing to set.mm. In any case, automatic tools, $j commands etc are dealing with symptoms of the problem, but not its root: neither mmj2 nor metamath-exe warn the user that their theorem proof doesn't use some hypothesis. -- 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/8d042a32-d901-42cd-9569-e903968da3c9n%40googlegroups.com.
