On November 26, 2020 11:09:53 AM PST, Norman Megill <[email protected]> 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.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/76833990-0CAA-49CD-9391-CB1FAE3C1FC8%40panix.com.
