This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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

Note that Lean's documentation is often inconsistent with its naming: e.g. a function called concat is said to append, a function called append is said to perform concatenation.

Comparison across languages

(m) means "mutates in place"

Language	Type	x :: xs	xs ++ [x]	xs ++ ys	xss[0] ++ xss[1] ++ ...
Lean	List	cons x xs	concat xs x	append xs ys	join xss
Lean	Fin n -> X	cons x xs	snoc xs x	append xs ys	We don't seem to have this. See below.*
Lean	Array	xs.insertAt! 0 x	xs.push x	append xs ys	xss.flatten and xss.join (duplication)
Python	list	xs.insert(0, x) (m)	xs.append(x) (m)	operator.concat(xs, ys) (though append and extend also work)	Various Pythonic ways to do this, no named function.
Python	deque	xs.appendleft(x) (m)	xs.appendright(x) (m)	operator.concat(xs, ys)	Various Pythonic ways to do this, no named function.
PHP	Array	array_unshift()	array_push()	array_merge($xs, $ys)	array_merge(...$xss)
Cryptol	Sequence (size-dependent)	[x] # xs	xs # [x]	(#) (doc: "append").	join xss
Haskell	List	(:)	snoc	(++) (doc: "append")	concat
Scala	List	(::) or, more generically, (+:)	(:+)	(++) or (:::) or List.concat	List.flatten
Scala	Array	(+:), or (+:=) for (m)	(:+), or (:+=) for (m)	(++) or Array.concat	Array.flatten
Rust	Vec<n>	Vec::insert, with argument index as 0	Vec::push, docs describe as append.	Vec::append	Vec::concat
F#	List	List.insertAt 0	List.insertAt (List.length)	List.append	List.concat
Common Lisp	List	cons	?	append, nconc (m)	(reduce #'append xss)
Mathematica	List/any head	Prepend	Append	Join/Catenate/Flatten (variadic)	Join/Catenate/Flatten

* This is how we could do join for tuples. But I don't believe we have it currently.

def finJoin : (Fin n → Fin m → α) ≃ (Fin (n * m) → α) :=
(Equiv.curry _ _ _).symm.trans ((finProdFinEquiv).arrowCongr (Equiv.refl _))

---