On 1/8/25 05:31, Richard Penner wrote:
I've got about 89 new theorems dating back to 2023 I would like to add to my Mathbox but cannot since they depend on work in Scott's mathbox.
That's reason enough for me to move the surreal number theorems to main. Our practice is to do so once we have two mathboxes that want to use a set of theorems.
> It's a problem compounded by the ordering of the mathboxes, which brings us back to Cantor's 19th century work on order types and ordinal numbers. :)
Heh, in set.mm we cut this Gordian know by not allowing dependencies between mathboxes regardless of their order. Pretty sure we have tooling to check that.
-- 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 visit https://groups.google.com/d/msgid/metamath/bcd4cb44-9c4d-4aed-8e3c-299f9e17994b%40panix.com.
