>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 appreciate if the first index of a word is 1not 0. The C language has arrays that begins et 0 and its a pain un the neck because you always have to deal with n - 1 expressions. I would also recommend that we have a part intermediate between the official one and the sandboxes so that people could mutualize their contributions. We could begin by those related to categories, topology, and words. We could call this part "Commons" by refererence to the fields belonging to the community in England before the XIXth century. -- FL My comments: 1. I have no issue with changing "concat" to "++". As for the Unicode symbol, I would lean towards just the simple "++" (two characters) rather than "⧺" (which looks weird to me, almost suggesting "not parallel" rather than 2 plus signs) but I'll go along with whatever people want. Frown is also acceptable to me (maybe even my personal first choice, given that it may be more common outside of computer science literature), maybe with .^. or ^^ or '` (upside down df-cnv) as the ASCII token. But if more people prefer ++ that is fine. 2. I assume you mean df-word. As Mario suggested, it would be helpful if you provide the label of what you are referring to. I probably agree with you but I haven't worked with df-word, so others' comments would be more valid. I wonder if the awkward "( M ..^ N )" would largely be replaced by "( M ... N )". At this point, though, there are hundreds of theorems involved and probably a huge effort to convert. An important question is whether the literature typically starts with 0 or 1, which I don't know, and it's nice to be follow the literature convention when possible. (In C, I often start arrays with 1 because that's the way humans count. For me at least it leads to fewer bugs, and being able to use n instead of n-1 over and over saves typing and might even make up for the wasted memory space of the unused 0th entry. I imagine, though, that for "real" C programmers, counting from 0 is second nature so that when they see index n it mentally means the (n+1)th entry to them, so they don't need to use n-1.) 3. Note that we already have a section called "(Future - to be reviewed and classified)" http://us.metamath.org/mpeuni/mmtheorems.html#dtl:17.3 that was added primarily for the purpose of the "Commons" you mention. If people think that renaming it to "Commons" would be more intuitive, that's fine with me. Maybe "(Commons - to be reviewed and classified eventually)". Norm On Saturday, April 25, 2020 at 11:22:04 AM UTC-4, Benoit wrote: > > 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 "/_\". Also, since XOR is in Main, then > symmetric difference could be moved to Main too, in my opinion. > I could accept this. > > 3) Regarding logical connectives, I agree with Norm that > and/or/implies/iff/not/true/false are sufficient. It is also nice to have > XOR, NAND as examples, even though they are not used outside of propcalc. > It would be nice to have a subsection with NOR which parallels that for > NAND. No need for "negated implies", "(negated) is implied by", and > (negated) projections. > Well, I didn't mention T. and F. in my list. :) I think I've expressed a small distaste for T. in part because of the issues with defining it that we've discussed, but primarily because is very rarely used in mathematical literature beyond prop calc. For example, _V is almost always defined as {x|x=x}; I've never seen {x|T} in set theory literature, and I like to be faithful to literature whenever possible. For us, T. primarily serves a technical purpose inside of proofs as the heavy use of ~ trud shows, but I don't think it is used in any mainstream set.mm theorem beyond prop calc. NAND was originally added specifically to study Nicod's single axiom for prop calc. I don't know if NOR has been studied similarly. My preference is not to add it, but if people feel strongly I guess I would accept it. Norm -- 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/7980f9c7-3df5-4318-a25b-21867f1bcc7f%40googlegroups.com.
