Thanks for asking about this.
Here's a pull request to add this case to the metamath-exe testsuite:
https://github.com/metamath/metamath-exe/pull/83
On 5/8/22 05:17, Glauco wrote:
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
<https://groups.google.com/d/msgid/metamath/d6dd174f-b563-4adb-ad06-5c2531e0520en%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 on the web visit
https://groups.google.com/d/msgid/metamath/a3a44504-6529-d1ad-5ef6-8514c3d9c9ce%40panix.com.
