Skip to content

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

Eric Wieser edited this page Dec 4, 2023 · 34 revisions

This follows on from ideas in:

Comparison across languages

(m) means "mutates in place"

| Language | x :: xs | xs ++ [x] | xs ++ ys |--|--|--| | Lean List | cons x xs | concat x xs | append xs ys | Python | xs.insert(0, x) | xs.append(x) (m) | operator.concat

Clone this wiki locally