Documentation

Mathlib.Data.List.DropRight

Dropping or taking from lists on the right #

Taking or removing element from the tail end of a list

Main definitions #

Implementation detail #

The two predicate-based methods operate by performing the regular "from-left" operation on List.reverse, followed by another List.reverse, so they are not the most performant. The other two rely on List.length l so they still traverse the list twice. One could construct another function that takes a L : ℕ and use L - n. Under a proof condition that L = l.length, the function would do the right thing.

def List.rdrop {α : Type u_1} (l : List α) (n : ) :
List α

Drop n elements from the tail end of a list.

Equations
@[simp]
theorem List.rdrop_nil {α : Type u_1} (n : ) :
@[simp]
theorem List.rdrop_zero {α : Type u_1} (l : List α) :
l.rdrop 0 = l
theorem List.rdrop_eq_reverse_drop_reverse {α : Type u_1} (l : List α) (n : ) :
@[simp]
theorem List.rdrop_concat_succ {α : Type u_1} (l : List α) (n : ) (x : α) :
(l ++ [x]).rdrop (n + 1) = l.rdrop n
def List.rtake {α : Type u_1} (l : List α) (n : ) :
List α

Take n elements from the tail end of a list.

Equations
@[simp]
theorem List.rtake_nil {α : Type u_1} (n : ) :
@[simp]
theorem List.rtake_zero {α : Type u_1} (l : List α) :
l.rtake 0 = []
theorem List.rtake_eq_reverse_take_reverse {α : Type u_1} (l : List α) (n : ) :
@[simp]
theorem List.rtake_concat_succ {α : Type u_1} (l : List α) (n : ) (x : α) :
(l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]
def List.rdropWhile {α : Type u_1} (p : αBool) (l : List α) :
List α

Drop elements from the tail end of a list that satisfy p : α → Bool. Implemented naively via List.reverse

Equations
@[simp]
theorem List.rdropWhile_nil {α : Type u_1} (p : αBool) :
theorem List.rdropWhile_concat {α : Type u_1} (p : αBool) (l : List α) (x : α) :
@[simp]
theorem List.rdropWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
@[simp]
theorem List.rdropWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
rdropWhile p (l ++ [x]) = l ++ [x]
theorem List.rdropWhile_singleton {α : Type u_1} (p : αBool) (x : α) :
theorem List.rdropWhile_last_not {α : Type u_1} (p : αBool) (l : List α) (hl : rdropWhile p l []) :
¬p ((rdropWhile p l).getLast hl) = true
theorem List.rdropWhile_prefix {α : Type u_1} (p : αBool) (l : List α) :
@[simp]
theorem List.rdropWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
rdropWhile p l = [] ∀ (x : α), x lp x = true
@[simp]
theorem List.dropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
dropWhile p l = l ∀ (hl : 0 < l.length), ¬p (l.get 0, hl) = true
@[simp]
theorem List.rdropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
rdropWhile p l = l ∀ (hl : l []), ¬p (l.getLast hl) = true
theorem List.dropWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
theorem List.rdropWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
def List.rtakeWhile {α : Type u_1} (p : αBool) (l : List α) :
List α

Take elements from the tail end of a list that satisfy p : α → Bool. Implemented naively via List.reverse

Equations
@[simp]
theorem List.rtakeWhile_nil {α : Type u_1} (p : αBool) :
theorem List.rtakeWhile_concat {α : Type u_1} (p : αBool) (l : List α) (x : α) :
@[simp]
theorem List.rtakeWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
@[simp]
theorem List.rtakeWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
theorem List.rtakeWhile_suffix {α : Type u_1} (p : αBool) (l : List α) :
@[simp]
theorem List.rtakeWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
rtakeWhile p l = l ∀ (x : α), x lp x = true
@[simp]
theorem List.rtakeWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
rtakeWhile p l = [] ∀ (hl : l []), ¬p (l.getLast hl) = true
theorem List.mem_rtakeWhile_imp {α : Type u_1} {p : αBool} {l : List α} {x : α} (hx : x rtakeWhile p l) :
p x = true
theorem List.rtakeWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
theorem List.rdrop_add {α : Type u_1} {l : List α} (i j : ) :
(l.rdrop i).rdrop j = l.rdrop (i + j)
@[simp]
theorem List.rdrop_append_length {α : Type u_1} {l₁ l₂ : List α} :
(l₁ ++ l₂).rdrop l₂.length = l₁
theorem List.rdrop_append_of_le_length {α : Type u_1} {l₁ l₂ : List α} (k : ) :
k l₂.length(l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
@[simp]
theorem List.rdrop_append_length_add {α : Type u_1} {l₁ l₂ : List α} (k : ) :
(l₁ ++ l₂).rdrop (l₂.length + k) = l₁.rdrop k