English
An auxiliary function for defining permutations: permutationsAux2 t ts r computes a transformed pair by inserting t into ts in all positions and prepending results with r.
Русский
Вспомогательная функция для определения перестановок: permutationsAux2 t ts r вычисляет пару, полученную вставкой t во все позиции в ts и добавлением результатов в r.
LaTeX
$$$\\mathrm{permutationsAux2}(t,ts,r) = (ys, zs)$ где $ys$ получено вставкой $t$ во все позиции в $ts$, а $zs = (insert\\_left(ts,t,ts).map f) \\ ++ r$$$
Lean4
/-- An auxiliary function for defining `permutations`. `permutationsAux2 t ts r ys f` is equal to
`(ys ++ ts, (insert_left ys t ts).map f ++ r)`, where `insert_left ys t ts` (not explicitly
defined) is the list of lists of the form `insert_nth n t (ys ++ ts)` for `0 ≤ n < length ys`.
permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
([1, 2, 3, 4, 5, 6],
[[10, 1, 2, 3, 4, 5, 6],
[1, 10, 2, 3, 4, 5, 6],
[1, 2, 10, 3, 4, 5, 6]]) -/
def permutationsAux2 (t : α) (ts : List α) (r : List β) : List α → (List α → β) → List α × List β
| [], _ => (ts, r)
| y :: ys, f =>
let (us, zs) := permutationsAux2 t ts r ys (fun x : List α => f (y :: x))
(y :: us, f (t :: y :: us) :: zs)
