Lean4
/-- `permutations'Aux t ts` inserts `t` into every position in `ts`, including the last.
This function is intended for use in specifications, so it is simpler than `permutationsAux2`,
which plays roughly the same role in `permutations`.
Note that `(permutationsAux2 t [] [] ts id).2` is similar to this function, but skips the last
position:
permutations'Aux 10 [1, 2, 3] =
[[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
(permutationsAux2 10 [] [] [1, 2, 3] id).2 =
[[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]] -/
@[simp]
def permutations'Aux (t : α) : List α → List (List α)
| [] => [[t]]
| y :: ys => (t :: y :: ys) :: (permutations'Aux t ys).map (cons y)
