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...
Alexander -- 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/68abe88e-2a7f-44d6-a001-475abc4f5ed4%40googlegroups.com.
