On Friday, January 14, 2022 at 1:51:53 PM UTC+1 Benoit wrote:
> I think we can separate both issues (the question of symbols for Even/Odd > being discussed on github, and the question of mutual mathbox uses). > Probably the best option is: if mathbox A uses the theorem xxx proved in > mathbox B, then add to mathbox A the axiom ax-xxx with exactly the same > statement as xxx and put a comment like "Duplicate of ~ xxx." > > This is a good idea (for an intermediate solution), therefore I have adapted my mathbox as Benoît proposed in my current PR https://github.com/metamath/set.mm/pull/2434. -- 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/413e9736-04cd-4371-a1b2-5872815ffdd1n%40googlegroups.com.
