Skip to content

Alternate names for `List.concat` and `List.append`

lines edited this page Dec 4, 2023 · 34 revisions

This follows on from ideas in:

Comparison across languages

(m) means "mutates in place"

Language Type x :: xs xs ++ [x] xs ++ ys
Lean List cons x xs concat xs x append xs ys
Lean Fin n -> X cons x xs snoc xs x append xs ys
Python list xs.insert(0, x) (m) xs.append(x) (m) operator.concat(xs, ys)
Python deque xs.appendleft(x) (m) xs.appendright(x) (m) operator.concat(xs, ys)
PHP Array array_unshift() array_push() array_merge()