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 <http://us.metamath.org/mpegif/expcncf.html> 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.
