Re: [Metamath] Re: New community verifier?

2020-11-26 Thread David A. Wheeler
On November 27, 2020 12:14:09 AM EST, Mario Carneiro wrote: >Hi All, > >I've just put the finishing touches on the mm0-rs HTML generator, which >makes pages such as >https://digama0.github.io/mm0/peano/thms/addass.html . >As should be pretty obvious, it's based on the metamath web page >display,

Re: [Metamath] Re: New community verifier?

2020-11-26 Thread Mario Carneiro
Hi All, I've just put the finishing touches on the mm0-rs HTML generator, which makes pages such as https://digama0.github.io/mm0/peano/thms/addass.html . As should be pretty obvious, it's based on the metamath web page display, but I would like to make it a bit more interactive, possibly

Re: [Metamath] Re: Incorrect definition reference in HTML page for ILE 'wal'

2020-11-26 Thread Jim Kingdon
On November 26, 2020 11:09:53 AM PST, Norman Megill wrote: >df-tru has been nothing but trouble, and sometimes I rue the day it >escaped >from a mathbox. :) Haha yeah it has been, hasn't it? I suspect we're pretty much stuck with it, especially in iset.mm, because

[Metamath] Re: Incorrect definition reference in HTML page for ILE 'wal'

2020-11-26 Thread Norman Megill
The current web page generation algorithm looks for the next "$a |-" using the syntax. If its label starts with "ax-" the syntax is called "primitive" on the web page. I'll have to add an exception for the case of wal, which I'll try to do in the next release of metamath.exe. df-tru has been

Re: [Metamath] Incorrect definition reference in HTML page for ILE 'wal'

2020-11-26 Thread Jim Kingdon
Interesting. This is presumably a consequence of the recent (ish) change to the definition of the true constant and is also found at http://us.metamath.org/mpeuni/wal.html Because this message is generated programmatically, the fix probably isn't as simple as one might think. So I guess I'll

[Metamath] Incorrect definition reference in HTML page for ILE 'wal'

2020-11-26 Thread Marnix Klooster
Hello Norm, others, A quick bug report. I just noted that http://us.metamath.org/ileuni/wal.html incorrectly says "See definition df-tru 1245 for more information." It should probably instead say, "This syntax is primitive. The first axiom using it is