Concatenation operators
Hi,
I was wondering whether we should prefer to use :::
or ++
for list concatenation (since they both essentially do the same thing on lists).
Furthermore, should we use ::
or +:
for element concatenation on lists?
Are both operators fine or is one deprecated?