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

Jump to bottom

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 | [xs] -> xss |--|--|--|--|--| | 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() | Cryptol | Sequence (size-dependent) | [x] # xs | xs # [x] | (#), called "append" in documentation.