On Friday, January 14, 2022 at 5:02:53 AM UTC+1 Thierry Arnoux wrote:
> ...
>
> Anyway, I'd also like to point out that technically, nothing prevents
> Alexander (sorry for the mix-up in my previous mail) to use theorems from
> my Mathbox; this rule is nowhere enforced. Maybe a short comment that this
> goes against the usage and why we chose to make an exception would also
> work!
>
> Actually, it *is enforced* not to use theorems of other's mathboxes: on
running "verify markup", there will be warning, for example:
?Warning: The proof of "tgoldbachgtX" in the mathbox for Alexander van der
Vekens references "tgoldbachgt" in the mathbox for Thierry Arnoux.
If it is not accepted to have a dedicated symbol "Odd" (and if we have such
a symbol, we also should have a symbol "Even" for symmetry reasons,
although it would not really be needed), I already though of using
Thierry's local `O`, but let's discuss this further in the github issue
#2433 opend by Jim.
--
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/7f51e48f-3e54-4034-a4b0-4edad72e1501n%40googlegroups.com.
