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 On Thursday, November 26, 2020 at 5:28:55 AM UTC-5 Marnix Klooster wrote: > Hello Norm, others, > > A quick bug report. I just noted that > http://us.metamath.org/ileuni/wal.html incorrectly says "See definition > df-tru <http://us.metamath.org/ileuni/df-tru.html> 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 > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/902aa7eb-6297-463f-9d00-305263eb2e08n%40googlegroups.com.
