Documentation

Batteries.Data.List.EraseIdx

Basic properties of List.eraseIdx #

List.eraseIdx l k erases k-th element of l : List α. If k ≥ length l, then it returns l.

@[simp]
theorem List.eraseIdx_zero {α : Type u} (l : List α) :
l.eraseIdx 0 = l.tail
theorem List.eraseIdx_eq_take_drop_succ {α : Type u} (l : List α) (i : Nat) :
l.eraseIdx i = List.take i l ++ List.drop (i + 1) l
theorem List.eraseIdx_sublist {α : Type u} (l : List α) (k : Nat) :
(l.eraseIdx k).Sublist l
theorem List.eraseIdx_subset {α : Type u} (l : List α) (k : Nat) :
l.eraseIdx k l
@[simp]
theorem List.eraseIdx_eq_self {α : Type u} {l : List α} {k : Nat} :
l.eraseIdx k = l l.length k
theorem List.eraseIdx_of_length_le {α : Type u} {l : List α} {k : Nat} :
l.length kl.eraseIdx k = l

Alias of the reverse direction of List.eraseIdx_eq_self.

theorem List.eraseIdx_append_of_lt_length {α : Type u} {l : List α} {k : Nat} (hk : k < l.length) (l' : List α) :
(l ++ l').eraseIdx k = l.eraseIdx k ++ l'
theorem List.eraseIdx_append_of_length_le {α : Type u} {l : List α} {k : Nat} (hk : l.length k) (l' : List α) :
(l ++ l').eraseIdx k = l ++ l'.eraseIdx (k - l.length)
theorem List.IsPrefix.eraseIdx {α : Type u} {l : List α} {l' : List α} (h : l <+: l') (k : Nat) :
l.eraseIdx k <+: l'.eraseIdx k
theorem List.mem_eraseIdx_iff_getElem {α : Type u} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Fin l.length), i k l[i] = x
@[deprecated List.mem_eraseIdx_iff_getElem]
theorem List.mem_eraseIdx_iff_get {α : Type u} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Fin l.length), i k l.get i = x
theorem List.mem_eraseIdx_iff_getElem? {α : Type u} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Nat), i k l[i]? = some x
@[deprecated List.mem_eraseIdx_iff_getElem?]
theorem List.mem_eraseIdx_iff_get? {α : Type u} {x : α} {l : List α} {k : Nat} :
x l.eraseIdx k ∃ (i : Nat), i k l.get? i = some x