-
Notifications
You must be signed in to change notification settings - Fork 343
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 |
[xs] -> xss |
---|---|---|---|---|---|
Lean | List |
cons x xs |
concat xs x |
append xs ys |
Lean.join |
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) (though append and extend also work) |
|
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] |
(#) (doc: "append"). |
join |
Haskell | List | (:) |
snoc |
(++) (doc: "append") |
concat |