I was thinking the same thing, every integer is even or odd is a good
example of XOR but I wouldn't recommend it for most uses (and even for nneo
we will probably want the iff version because it has more theorems about
it).
On Sat, Apr 25, 2020 at 7:39 PM Jim Kingdon wrote:
> > Thinking of it
> Thinking of it as "either one side or the other side is true but not both"
> doesn't seem to convey the same meaning.
I guess what got me down this whole line of thinking was the text "A positive
integer is even or odd but not both" from the comment to
http://us.metamath.org/mpeuni/nneo.html
Posted per request of FL.
Forwarded Message
Subject: Operators
Date: Sat, 25 Apr 2020 21:21:07 +0200 (CEST)
From: fl
To: Megill Norman
Let's agree: of course the opinion that we should confine ourselvesto the 5
classical operators for the formulation of the theorems. The
On Saturday, April 25, 2020 at 1:33:20 PM UTC-4, Jim Kingdon wrote:
>
> With respect to exclusive or, there are a lot of theorems in set.mm which
> use ?? <-> -. ?? (examples: sotric , posn , nneo , nltpnft ). At least some
> of these can be productively thought of as exclusive or and may
With respect to exclusive or, there are a lot of theorems in set.mm which use
?? <-> -. ?? (examples: sotric , posn , nneo , nltpnft ). At least some of
these can be productively thought of as exclusive or and may benefit from
notating them as exclusive or. In set.mm this is presumably just a
>From FL:
Forwarded Message
Subject: ++, indices and Commons
Date: Sat, 25 Apr 2020 11:53:57 +0200 (CEST)
From: fl
To: Megill Norman
Hi Norm,
could you post this:
Yes I made a mistake. Scott Fenton uses (++) and not ++. So the symbol ++
is available.
I would also
1) I do not have strong opinions for concatenation: either "concat", which
is self-explanatory, or "++", which might be a bit more obscure, is good
(better than the other alternatives).
2) As for symmetric difference, $\triangle$ is the more standard notation,
with a nice ascii version being
On Sat, 25 Apr 2020 00:49:41 -0700 (PDT), "'Alexander van der Vekens' via
Metamath" wrote:
> I propose to use (the new version of) frlmgsum in step 85 and to replace
> step 84 by ...
That fixes it! Thanks. I repaired the $d provisos, cleaned up the
comments, and created a pull request to add
I propose to use (the new version of) frlmgsum in step 85 and to replace
step 84 by
d7::eqid |- ( k
e. ( 0 ... N )
|-> ( n e. ( 1 ... N ) |-> ( ( w ` k ) x. C ) ) )
= ( k
e. ( 0 ... N
I also like the idea to replace concat by a symbol, and I agree with David
that we should decide between frown and doubleplus. As ASCII symbol for
frown we could take '^' (only one character more than ++). From a visual
point of view, I would prefer the frown (looks like joining the two
The problem is that the proof uses an old version of frlmgsum: Either
frlmgsumOLD (deprecated!) must be used in step 85, or step 84 must be
adapted to comply with the new version of frlmgsum.
Alexander
On Saturday, April 25, 2020 at 7:41:56 AM UTC+2, David A. Wheeler wrote:
>
> On Fri, 10 Apr
11 matches
Mail list logo
