modifyHead #
@[simp]
@[simp]
@[simp]
@[simp]
theorem
List.getElem_modifyHead_zero
{α : Type u_1}
{l : List α}
{f : α → α}
{h : 0 < (modifyHead f l).length}
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
modifyTailIdx #
@[simp]
theorem
List.modifyTailIdx_modifyTailIdx
{α : Type u_1}
{f g : List α → List α}
(m n : Nat)
(l : List α)
:
modifyTailIdx g (m + n) (modifyTailIdx f n l) = modifyTailIdx (fun (l : List α) => modifyTailIdx g m (f l)) n l
modify #
@[simp]