wff and class definitions don't work again

[GinoGiotto]

Example: https://metamath.tirix.org/mpests/wmo.html

It shows "Could not format assertion : Unknown statement" again.

[tirix]

That's actually a different case, previously I fixed only hypotheses, this time I also fixed definitions. This should be fixed with #27.

[GinoGiotto]

I don't understand, the official metamath page seems to differ from the metamath-web one.

Taking wmo as example (don't mind that I'm using dark mode):

The metamath-page https://us.metamath.org/mpeuni/wmo.html shows:

While the corresponding metamath-web https://metamath.tirix.org/mpests/wmo.html shows:

The first shows a wff type, while the second shows a turnstile (the official website shows $f hypotheses as well, but that's maybe a topic for other discussions).

[tirix]

The first shows a wff type, while the second shows a turnstile

Yes that's wrong, turnstile means provable, and that assertion is not provable in general, it's just a syntax definition. I fix this specific problem in #28.

(the official website shows $f hypotheses as well, but that's maybe a topic for other discussions).

That's right! I had not noticed that before. There are two kinds of hypotheses defined by metamath:

• $f floating hypotheses (i.e. type declaration for variables)
• $e essential hypotheses (i.e. actual semantic hypotheses)

I systematically only display the essential hypotheses. I could make an exception for syntax definitions, and display floating hypotheses in this case, in order to match with the metamath pages.

[GinoGiotto]

I systematically only display the essential hypotheses. I could make an exception for syntax definitions, and display floating hypotheses in this case, in order to match with the metamath pages.

Sounds good, I'll open a new issue for this topic then.