modifyHead #
@[simp]
theorem
List.length_modifyHead
{α : Type u_1}
{f : α → α}
{l : List α}
:
(List.modifyHead f l).length = l.length
theorem
List.modifyHead_eq_set
{α : Type u_1}
[Inhabited α]
(f : α → α)
(l : List α)
:
List.modifyHead f l = l.set 0 (f (l[0]?.getD default))
@[simp]
theorem
List.modifyHead_eq_nil_iff
{α : Type u_1}
{f : α → α}
{l : List α}
:
List.modifyHead f l = [] ↔ l = []
@[simp]
theorem
List.modifyHead_modifyHead
{α : Type u_1}
{l : List α}
{f : α → α}
{g : α → α}
:
List.modifyHead g (List.modifyHead f l) = List.modifyHead (g ∘ f) l
theorem
List.getElem_modifyHead
{α : Type u_1}
{l : List α}
{f : α → α}
{n : Nat}
(h : n < (List.modifyHead f l).length)
:
(List.modifyHead f l)[n] = if h' : n = 0 then f l[0] else l[n]
@[simp]
theorem
List.getElem_modifyHead_zero
{α : Type u_1}
{l : List α}
{f : α → α}
{h : 0 < (List.modifyHead f l).length}
:
(List.modifyHead f l)[0] = f l[0]
@[simp]
theorem
List.getElem_modifyHead_succ
{α : Type u_1}
{l : List α}
{f : α → α}
{n : Nat}
(h : n + 1 < (List.modifyHead f l).length)
:
(List.modifyHead f l)[n + 1] = l[n + 1]
theorem
List.getElem?_modifyHead
{α : Type u_1}
{l : List α}
{f : α → α}
{n : Nat}
:
(List.modifyHead f l)[n]? = if n = 0 then Option.map f l[n]? else l[n]?
@[simp]
theorem
List.getElem?_modifyHead_zero
{α : Type u_1}
{l : List α}
{f : α → α}
:
(List.modifyHead f l)[0]? = Option.map f l[0]?
@[simp]
theorem
List.getElem?_modifyHead_succ
{α : Type u_1}
{l : List α}
{f : α → α}
{n : Nat}
:
(List.modifyHead f l)[n + 1]? = l[n + 1]?
@[simp]
theorem
List.head_modifyHead
{α : Type u_1}
(f : α → α)
(l : List α)
(h : List.modifyHead f l ≠ [])
:
(List.modifyHead f l).head h = f (l.head ⋯)
@[simp]
theorem
List.head?_modifyHead
{α : Type u_1}
{l : List α}
{f : α → α}
:
(List.modifyHead f l).head? = Option.map f l.head?
@[simp]
theorem
List.tail_modifyHead
{α : Type u_1}
{f : α → α}
{l : List α}
:
(List.modifyHead f l).tail = l.tail
@[simp]
theorem
List.take_modifyHead
{α : Type u_1}
{f : α → α}
{l : List α}
{n : Nat}
:
List.take n (List.modifyHead f l) = List.modifyHead f (List.take n l)
@[simp]
theorem
List.drop_modifyHead_of_pos
{α : Type u_1}
{f : α → α}
{l : List α}
{n : Nat}
(h : 0 < n)
:
List.drop n (List.modifyHead f l) = List.drop n l
@[simp]
theorem
List.eraseIdx_modifyHead_zero
{α : Type u_1}
{f : α → α}
{l : List α}
:
(List.modifyHead f l).eraseIdx 0 = l.eraseIdx 0
@[simp]
theorem
List.eraseIdx_modifyHead_of_pos
{α : Type u_1}
{f : α → α}
{l : List α}
{n : Nat}
(h : 0 < n)
:
(List.modifyHead f l).eraseIdx n = List.modifyHead f (l.eraseIdx n)
modifyTailIdx #
@[simp]
theorem
List.eraseIdx_eq_modifyTailIdx
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyTailIdx List.tail n l
theorem
List.modifyTailIdx_add
{α : Type u_1}
(f : List α → List α)
(n : Nat)
(l₁ : List α)
(l₂ : List α)
:
List.modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyTailIdx f n l₂
modify #
@[simp]
theorem
List.modify_zero_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
:
List.modify f 0 (a :: l) = f a :: l
@[simp]
theorem
List.modify_succ_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
(n : Nat)
:
List.modify f (n + 1) (a :: l) = a :: List.modify f n l
theorem
List.modifyHead_eq_modify_zero
{α : Type u_1}
(f : α → α)
(l : List α)
:
List.modifyHead f l = List.modify f 0 l
@[simp]
theorem
List.modify_eq_nil_iff
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modify f n l = [] ↔ l = []
theorem
List.getElem?_modify
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modify f n l)[m]? = (fun (a : α) => if n = m then f a else a) <$> l[m]?
@[simp]
theorem
List.length_modify
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l).length = l.length
@[simp]
theorem
List.getElem?_modify_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l)[n]? = f <$> l[n]?
@[simp]
theorem
List.getElem?_modify_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modify f m l)[n]? = l[n]?
theorem
List.getElem_modify
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
(h : m < (List.modify f n l).length)
:
(List.modify f n l)[m] = if n = m then f l[m] else l[m]
@[simp]
theorem
List.getElem_modify_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(h : n < (List.modify f n l).length)
:
(List.modify f n l)[n] = f l[n]
@[simp]
theorem
List.getElem_modify_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
(h' : n < (List.modify f m l).length)
:
(List.modify f m l)[n] = l[n]
theorem
List.modify_eq_self
{α : Type u_1}
{f : α → α}
{n : Nat}
{l : List α}
(h : l.length ≤ n)
:
List.modify f n l = l
theorem
List.modify_modify_eq
{α : Type u_1}
(f : α → α)
(g : α → α)
(n : Nat)
(l : List α)
:
List.modify g n (List.modify f n l) = List.modify (g ∘ f) n l
theorem
List.modify_modify_ne
{α : Type u_1}
(f : α → α)
(g : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
List.modify g n (List.modify f m l) = List.modify f m (List.modify g n l)
theorem
List.modify_eq_set
{α : Type u_1}
[Inhabited α]
(f : α → α)
(n : Nat)
(l : List α)
:
List.modify f n l = l.set n (f (l[n]?.getD default))
theorem
List.modify_eq_take_drop
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modify f n l = List.take n l ++ List.modifyHead f (List.drop n l)
theorem
List.take_modify
{α : Type u_1}
(f : α → α)
(n : Nat)
(m : Nat)
(l : List α)
:
List.take n (List.modify f m l) = List.modify f m (List.take n l)
theorem
List.drop_modify_of_ge
{α : Type u_1}
(f : α → α)
(n : Nat)
(m : Nat)
(l : List α)
(h : n ≥ m)
:
List.drop m (List.modify f n l) = List.modify f (n - m) (List.drop m l)
theorem
List.eraseIdx_modify_of_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l).eraseIdx n = l.eraseIdx n
theorem
List.eraseIdx_modify_of_lt
{α : Type u_1}
(f : α → α)
(i : Nat)
(j : Nat)
(l : List α)
(h : j < i)
:
(List.modify f i l).eraseIdx j = List.modify f (i - 1) (l.eraseIdx j)
theorem
List.eraseIdx_modify_of_gt
{α : Type u_1}
(f : α → α)
(i : Nat)
(j : Nat)
(l : List α)
(h : j > i)
:
(List.modify f i l).eraseIdx j = List.modify f i (l.eraseIdx j)
theorem
List.modify_eraseIdx_of_lt
{α : Type u_1}
(f : α → α)
(i : Nat)
(j : Nat)
(l : List α)
(h : j < i)
:
List.modify f j (l.eraseIdx i) = (List.modify f j l).eraseIdx i
theorem
List.modify_eraseIdx_of_ge
{α : Type u_1}
(f : α → α)
(i : Nat)
(j : Nat)
(l : List α)
(h : j ≥ i)
:
List.modify f j (l.eraseIdx i) = (List.modify f (j + 1) l).eraseIdx i