I can't find test.mm , but I'm using this old post to keep mmverify.py
'issues' in one place.
I've written a TypeScript parser/verifier (one for .mm and one for .mmp
format) along the lines of mmverify.py , and I noticed that both my
verifier (and mmverify.py) don't catch an error that metamat.exe instead
does.
If you remove the line
vx.wal $f setvar x $.
from the block of
wal $a wff A. x ph $.
mmverify.py doesn't rise an error (of course, the first theorem that uses
wal, that is trujust, will rise an error).
Instead, metamath.exe, when reading set.mm (then, even before 'verify proof
*' ) returns this error:
The source has 200287 statements; 2648 are $a and 39659 are $p.
?Error on line 23725 of file "set.mm" at statement 4161, label "wal", type
"$a":
wal $a wff A. x ph $.
^
This variable does not occur in any active "$e" or "$f" hypothesis. All
variables in "$a" and "$p" statements must appear in at least one such
hypothesis.
?Error on line 23725 of file "set.mm" at statement 4161, label "wal", type
"$a":
wal $a wff A. x ph $.
The variable "x" does not appear in an active "$f" statement.
2 errors were found.
I've not looked at the spec in the metamath book, yet, to see if actually
any var is required to have a kind (when used in assertions).
If I'm not wrong, other verifiers are "based" on mmverify.mm , so I decided
to write this post.
Glauco
--
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/d6dd174f-b563-4adb-ad06-5c2531e0520en%40googlegroups.com.
