-
Notifications
You must be signed in to change notification settings - Fork 341
Alternate names for `List.concat` and `List.append`
Eric Wieser edited this page Dec 4, 2023
·
34 revisions
This follows on from ideas in:
- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/List.2Econcat.20and.20List.2Eappend/near/405811812
- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/append.20and.20concat/near/299602232
(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) |