Open GinoGiotto opened 11 months ago
Mentioned in: https://github.com/tirix/metamath-web/issues/26#issuecomment-1806945053
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.
Examples:
In this example wne has two class hypotheses. Official Metamath page: https://us.metamath.org/mpeuni/wne.html metamath-web: https://metamath.tirix.org/mpests/wne.html
wne
In this example wmo has a setvar and wff hypothesis: Official Metamath page https://us.metamath.org/mpeuni/wmo.html metamath-web: https://metamath.tirix.org/mpests/wmo.html
wmo
Beginner question: Can class definitions have $f hypotheses? With a quick search I didn't find any.
EDIT: nvm I found one: https://us.metamath.org/mpeuni/csb.html
Mentioned in: https://github.com/tirix/metamath-web/issues/26#issuecomment-1806945053
Examples:
In this example
wnehas two class hypotheses. Official Metamath page: https://us.metamath.org/mpeuni/wne.html metamath-web: https://metamath.tirix.org/mpests/wne.htmlIn this example
wmohas a setvar and wff hypothesis: Official Metamath page https://us.metamath.org/mpeuni/wmo.html metamath-web: https://metamath.tirix.org/mpests/wmo.htmlBeginner question: Can class definitions have $f hypotheses? With a quick search I didn't find any.
EDIT: nvm I found one: https://us.metamath.org/mpeuni/csb.html