Hi Shelby, David has gathered a set of test MM files for verifiers, which you can find here: https://github.com/david-a-wheeler/metamath-test
Glauco added there a set-dist.mm <https://github.com/david-a-wheeler/metamath-test/pull/1> file with a disjoint requirement removed to have a test for that case, but that is in no way minimal like your example, so it might be interesting to add your example to this repository. BR, _ Thierry On 30/12/2022 00:50, Shelby Doolittle wrote:
I'm working on a verifier for Metamath proofs, and I've reached the point of implementing disjoint requirements. I tried to make a minimal example of invalid use of disjoint variables, but the primary C metamath implementation seems to accept it. I'm likely doing something wrong, but I can't figure out what.
-- 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/cb2bd4b6-a354-2c25-4a1e-9f4aad4b0b2b%40gmx.net.
