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.
AFAIU, this file should not verify, but it does:
```
$c true num 0 1 != $.
$v x y $.
num_x $f num x $.
num_y $f num y $.
num_0 $a num 0 $.
num_1 $a num 1 $.
num_zero $a num 0 $.
num_one $a num 1 $.
${
$d x y $.
x_ne_y $a true x != y $.
$}
the1 $p true 0 != 0 $=
num_zero num_zero x_ne_y $.
```
--
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/052c1ef7-ca7e-4fbd-8e83-53323a1e1d4en%40googlegroups.com.
$c true num 0 1 != $.
$v x y $.
num_x $f num x $.
num_y $f num y $.
num_0 $a num 0 $.
num_1 $a num 1 $.
num_zero $a num 0 $.
num_one $a num 1 $.
${
$d x y $.
x_ne_y $a true x != y $.
$}
the1 $p true 0 != 0 $=
num_zero num_zero x_ne_y $.
