The comments on the concatentation symbol, in ASCII and in presentation, were all over the place. The symbol choice is not a deal-breaker for people :-). The (Unicode) presentation options came down to ++ or frown, while the ASCII representations came down to ++, '^', or concat.
I think the symbol and presentation of ++ was somewhat preferred by more people, and the people who preferred frown would be fine with ++. My attempt to (overly) simplify the preferences: ++: FL, Mario (doesn't want ASCII frown), David A. Wheeler (doesn't want ASCII frown) ++ _or_ "concat" as ASCII rep: Benoit [I think Benoit only focused on the ASCII form?] Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, not "concat"); Alexander also mentioned a compromise of "++" in ASCII but frown in presentation frown in presentation: Norman Megill (but no issue changing to ++) It was complicated to simplify the preferences; text snippets below. My apologies in advance if I didn't accurately represent a current position or missed somebody, please reply to correct! I'll create a pull request to switch ASCII symbol "concat" to "++", with presentation "++" (not the fancy Unicode symbol) per Norm's preference. Then Norm can decide if he wants to accept it. --- David A. Wheeler ======================= Norman Megill: 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. ... I'll also mention that Tarski used a frown symbol for concatenation in his 1965 paper. His notation is reproduced on p. 190 of the Metamath book, using the LaTeX symbol "\frown". Benoit: 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). Alexander: 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 operands), but I also would be happy with ++. As a compromise: we could take ++ as ASCII symbol and frown as display symbol - but this would be maybe too confusing... David A. Wheeler: I have a minor preference for ++, but it's not a big deal to me. In particular, I'd prefer "++" as the ASCII representation, with a Unicode display of U+29FA and \doubleplus in LaTeX (package unicode-math). This is somewhat common in Computer Science; Haskell uses "++" for concatenation, and many other programming languages use "+" for concatenation (but they can use types to figure out what overloaded operation was meant). I think ++ would make the ASCII display a little simpler, and many people think of "add" and "concatenate" as related... so having intentionally similar symbols has some mild advantages. Frown looks a little like intersection, even though there's no relationship, and that could be considered a negative for it. That said, frown has significant use, it's not terribly ambiguous, and it just works, so I'm not unhappy with it. ... I think frown and doubleplus are the contenders. (I don't like "no symbol", usually we try to make things obvious.) Mario: I like the idea of using ++ for concatenation, particularly in ascii notation, since I don't want to try to reproduce a frown symbol in ascii. I think the most common symbol for this is adjacency though. FL: (Fri, 24 April 2020 - kicked this off) I suggest that ++ replace concat. ... concat is very useful and the symbol is long. ++ is already used for concatenation in some computer languages. -- 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/E1jSjY5-0002Cc-Tk%40rmmprod06.runbox.
