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 Type x :: xs xs ++ [x] xs ++ ys
Lean List cons x xs concat x xs append xs ys
Python list xs.insert(0, x) xs.append(x) (m) operator.concat

Clone this wiki locally