Hi Jon, Yes, exactly. You may ask to move those theorems you need to the main part of set.mm. Chances are that if you need them, others may too. BR, _ Thierry
> Le 30 mai 2019 à 17:28, Jon P <[email protected]> a écrit : > > So I finally have a little time to work on this. > > One issue I have, when my proofs are at the very end of set.mm they work > fine. However when I move them to my mathbox I get errors like these, > > E-LA-0101 Theorem cnioobibld: compressed proof contains invalid statement > label, not found in Statement Table. Label position within the compressed > proof's parentheses = 28. Statement label = ioovolcl > E-LA-0101 Theorem itexp: compressed proof contains invalid statement label, > not found in Statement Table. Label position within the compressed proof's > parentheses = 41. Statement label = expcncf > > I believe this is because those theorems are after my mathbox, for example > expcncf is in the mathbox of Glauco Siliprandi. How is it recommended to work > with this? > -- > 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/4b8fd563-5a20-4e3f-97ca-9550253f8d89%40googlegroups.com. -- 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/5E5BEAB9-F65A-49A3-B30E-A9DFBFE79A10%40gmx.net.
