# Documentation

Mathlib.Data.List.Rdrop

# Dropping or taking from lists on the right #

Taking or removing element from the tail end of a list

## Main defintions #

• rdrop n: drop n : ℕ elements from the tail
• rtake n: take n : ℕ elements from the tail
• rdropWhile p: remove all the elements from the tail of a list until it finds the first element for which p : α → Bool returns false. This element and everything before is returned.
• rtakeWhile p: Returns the longest terminal segment of a list for which p : α → Bool returns true.

## 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 : ) :
List.rdrop [] n = []
@[simp]
theorem List.rdrop_zero {α : Type u_1} (l : List α) :
= l
@[simp]
theorem List.rdrop_concat_succ {α : Type u_1} (l : List α) (n : ) (x : α) :
List.rdrop (l ++ [x]) (n + 1) =
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 : ) :
List.rtake [] n = []
@[simp]
theorem List.rtake_zero {α : Type u_1} (l : List α) :
= []
@[simp]
theorem List.rtake_concat_succ {α : Type u_1} (l : List α) (n : ) (x : α) :
List.rtake (l ++ [x]) (n + 1) = ++ [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 : α) :
List.rdropWhile p (l ++ [x]) = if p x = true then else l ++ [x]
@[simp]
theorem List.rdropWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
List.rdropWhile p (l ++ [x]) =
@[simp]
theorem List.rdropWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
List.rdropWhile p (l ++ [x]) = l ++ [x]
theorem List.rdropWhile_singleton {α : Type u_1} (p : αBool) (x : α) :
List.rdropWhile p [x] = if p x = true then [] else [x]
theorem List.rdropWhile_last_not {α : Type u_1} (p : αBool) (l : List α) (hl : []) :
theorem List.rdropWhile_prefix {α : Type u_1} (p : αBool) (l : List α) :
<+: l
@[simp]
theorem List.rdropWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
= [] ∀ (x : α), x lp x = true
@[simp]
theorem List.dropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (hl : 0 < ), ¬p (List.nthLe l 0 hl) = true
@[simp]
theorem List.rdropWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (hl : l []), ¬p (List.getLast l 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 : α) :
List.rtakeWhile p (l ++ [x]) = if p x = true then ++ [x] else []
@[simp]
theorem List.rtakeWhile_concat_pos {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : p x = true) :
List.rtakeWhile p (l ++ [x]) = ++ [x]
@[simp]
theorem List.rtakeWhile_concat_neg {α : Type u_1} (p : αBool) (l : List α) (x : α) (h : ¬p x = true) :
List.rtakeWhile p (l ++ [x]) = []
theorem List.rtakeWhile_suffix {α : Type u_1} (p : αBool) (l : List α) :
<:+ l
@[simp]
theorem List.rtakeWhile_eq_self_iff {α : Type u_1} {p : αBool} {l : List α} :
= l ∀ (x : α), x lp x = true
@[simp]
theorem List.rtakeWhile_eq_nil_iff {α : Type u_1} {p : αBool} {l : List α} :
= [] ∀ (hl : l []), ¬p (List.getLast l hl) = true
theorem List.mem_rtakeWhile_imp {α : Type u_1} {p : αBool} {l : List α} {x : α} (hx : x ) :
p x = true
theorem List.rtakeWhile_idempotent {α : Type u_1} (p : αBool) (l : List α) :
=