List.modifyLast

theorem List.modifyLast_concat {α : Type u_1} (f : α → α) (a : α) (l : List α) : modifyLast f (l ++ [a]) = l ++ [f a]

@[deprecated List.modifyLast_concat (since := "2025-02-07")]

theorem List.modifyLast_append_one {α : Type u_1} (f : α → α) (a : α) (l : List α) : modifyLast f (l ++ [a]) = l ++ [f a]

Alias of List.modifyLast_concat.

theorem List.modifyLast_append_of_right_ne_nil {α : Type u_1} (f : α → α) (l₁ l₂ : List α) : l₂ ≠ [] → modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

@[deprecated List.modifyLast_append_of_right_ne_nil (since := "2025-02-07")]

theorem List.modifyLast_append {α : Type u_1} (f : α → α) (l₁ l₂ : List α) : l₂ ≠ [] → modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂

Alias of List.modifyLast_append_of_right_ne_nil.