metamath-knife also permits it. I think not all mm verifiers support it though; I originally advocated for adding this rule to simplify verifiers that don't do scoped c/v (e.g. because they build a grammar for the database and use that to check everything).
On Mon, Feb 24, 2025 at 8:26 PM Glauco <[email protected]> wrote: > I've tested the example myself, and the Metamath program verifies it > without errors. > > Given the explicit statement in the book, I lean toward considering this > as a potential issue in metamath-exe rather than an erratum for the book. > > How does metamathknife handle this case? > > -- > 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/a0a5ed40-75bd-4413-af03-a472c37c369fn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/a0a5ed40-75bd-4413-af03-a472c37c369fn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSucNROPkz6%2BuP5pF2nbYerTsg30Ris7NpQmV%2BuKnLP5Zw%40mail.gmail.com.
