is there a test for non unique label

[glacode]

I was searching the test folder for a test checking for label duplication (I was not able to find one).
I suspect some parser (mine, to name one...) does not check for this.

Here's an example of the metamath output

MM> re id.mm
Reading source file "id.mm"... 714 bytes
714 bytes were read into the source buffer.
The source has 31 statements; 4 are $a and 4 are $p.

?Error on line 12 of file "id.mm" at statement 27, label "mpd", type "$p":
mpd $p |- ( ph -> ch ) $= ( wi a2i ax-mp ) ABFACFDABCEGH $. $}
^^^
This label is declared more than once. All labels must be unique.

BR
Glauco

[digama0]

To contribute a test, create an id.in file containing e.g. ve p *, and an id.mm file containing the test case, then run tests/run_test.sh --bless id to create the expected out file.

By the way, although your snippet indicates that metamath.exe does this check at parse time, I think it is also reasonable to do the check only at verification time. Obviously you have to check for it eventually, because otherwise you could have two theorems with different statements and the same name and it would be ambiguous what subsequent theorems are referring to.