Incorrect definition reference in HTML page for ILE 'wal'

[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 ...", like http://us.metamath.org/ileuni/wex.html says.

Thanks.

-Marnix

--

Marnix Klooster
marnix....@gmail.com

[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 leave this to "Norm, others".

[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 nothing but trouble, and sometimes I rue the day it escaped from a mathbox. :)

Norm

[Jim Kingdon]

On November 26, 2020 11:09:53 AM PST, Norman Megill <n...@alum.mit.edu> 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 http://us.metamath.org/ileuni/dfnot.html is so central to how a lot of people think about intuitionistic negation. But it is funny that defining true and false constants sounds easy yet causes various annoyances.