Post #2479121
2026-05-09 20:23 UTC
@olynch@mathstodon.xyz @MartinEscardo@mathstodon.xyz The error handling which is different is that if I take any theorem and remove the distinct variable constraint ($d), metamath-knife says 'Disjoint variable constraint violated' and no further details. metamath-exe gives 'Variables "A" and "f" do not have a disjoint variable requirement in the assertion being proved' (and likewise for every pair of variables missing the constraint).
Replies (1)
-
@soaproot@sfba.social 2026-05-09 20:27
@olynch@mathstodon.xyz @MartinEscardo@mathstodon.xyz I realize that I might have made it sound like I was talking about parse errors. But as far as I've noticed both of these two verifiers lose their minds in roughly similar ways if I do something like omit a "$}" (the ${ and $} syntaxes form nested pairs and so making them unbalanced is similar to unbalanced pairs in a lot of syntaxes - the scopes get all mixed up and so on).