mem #
@[simp]
next? #
get? #
modifyNth #
@[simp]
@[simp]
theorem
List.modifyNth_zero_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
:
List.modifyNth f 0 (a :: l) = f a :: l
@[simp]
theorem
List.modifyNth_succ_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
(n : Nat)
:
List.modifyNth f (n + 1) (a :: l) = a :: List.modifyNth f n l
theorem
List.eraseIdx_eq_modifyNthTail
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyNthTail List.tail n l
@[deprecated List.eraseIdx_eq_modifyNthTail]
theorem
List.removeNth_eq_nth_tail
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyNthTail List.tail n l
Alias of List.eraseIdx_eq_modifyNthTail.
theorem
List.getElem?_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modifyNth f n l)[m]? = (fun (a : α) => if n = m then f a else a) <$> l[m]?
@[deprecated List.getElem?_modifyNth]
theorem
List.get?_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modifyNth f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m
theorem
List.modifyNthTail_add
{α : Type u_1}
(f : List α → List α)
(n : Nat)
(l₁ : List α)
(l₂ : List α)
:
List.modifyNthTail f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyNthTail f n l₂
@[simp]
theorem
List.modify_get?_length
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l).length = l.length
@[simp]
theorem
List.getElem?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l)[n]? = f <$> l[n]?
@[deprecated List.getElem?_modifyNth_eq]
theorem
List.get?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modifyNth f n l).get? n = f <$> l.get? n
@[simp]
theorem
List.getElem?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modifyNth f m l)[n]? = l[n]?
@[deprecated List.getElem?_modifyNth_ne]
theorem
List.get?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m : Nat}
{n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modifyNth f m l).get? n = l.get? n
theorem
List.modifyNth_eq_take_drop
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modifyNth f n l = List.take n l ++ List.modifyHead f (List.drop n l)
set #
theorem
List.set_eq_modifyNth
{α : Type u_1}
(a : α)
(n : Nat)
(l : List α)
:
l.set n a = List.modifyNth (fun (x : α) => a) n l
theorem
List.modifyNth_eq_set_get?
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modifyNth f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l
theorem
List.modifyNth_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
List.modifyNth f n l = l.set n (f (l.get ⟨n, h⟩))
@[deprecated List.length_eraseIdx]
Alias of List.length_eraseIdx.
splitAt #
theorem
List.splitAt_eq
{α : Type u_1}
(n : Nat)
(l : List α)
:
List.splitAt n l = (List.take n l, List.drop n l)
eraseP #
@[simp]
theorem
List.extractP_eq_find?_eraseP
{α : Type u_1}
{p : α → Bool}
(l : List α)
:
List.extractP p l = (List.find? p l, List.eraseP p l)
theorem
List.extractP_eq_find?_eraseP.go
{α : Type u_1}
{p : α → Bool}
(l : List α)
(acc : Array α)
(xs : List α)
:
l = acc.data ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.data ++ List.eraseP p xs)
erase #
@[deprecated List.Sublist.erase]
theorem
List.sublist.erase
{α : Type u_1}
[BEq α]
(a : α)
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
(l₁.erase a).Sublist (l₂.erase a)
Alias of List.Sublist.erase.
replaceF #
theorem
List.replaceF_cons
{α : Type u_1}
{p : α → Option α}
(a : α)
(l : List α)
:
List.replaceF p (a :: l) = match p a with
| none => a :: List.replaceF p l
| some a' => a' :: l
theorem
List.replaceF_cons_of_none
{α : Type u_1}
{a : α}
{l : List α}
(p : α → Option α)
(h : p a = none)
:
List.replaceF p (a :: l) = a :: List.replaceF p l
theorem
List.replaceF_of_forall_none
{α : Type u_1}
{p : α → Option α}
{l : List α}
(h : ∀ (a : α), a ∈ l → p a = none)
:
List.replaceF p l = l
@[simp]
theorem
List.length_replaceF :
∀ {α : Type u_1} {f : α → Option α} {l : List α}, (List.replaceF f l).length = l.length
disjoint #
union #
theorem
List.union_def
{α : Type u_1}
[BEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁ ∪ l₂ = List.foldr List.insert l₂ l₁
inter #
theorem
List.inter_def
{α : Type u_1}
[BEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁ ∩ l₂ = List.filter (fun (x : α) => List.elem x l₂) l₁
product #
monadic operations #
theorem
List.forIn_eq_bindList
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
[LawfulMonad m]
(f : α → β → m (ForInStep β))
(l : List α)
(init : β)
:
forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
diff #
theorem
List.diff_eq_foldl
{α : Type u_1}
[BEq α]
[LawfulBEq α]
(l₁ : List α)
(l₂ : List α)
:
l₁.diff l₂ = List.foldl List.erase l₁ l₂
drop #
Chain #
@[simp]
theorem
List.chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
:
List.Chain R a (b :: l) ↔ R a b ∧ List.Chain R b l
theorem
List.rel_of_chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
(p : List.Chain R a (b :: l))
:
R a b
theorem
List.chain_of_chain_cons
{α : Type u_1}
{R : α → α → Prop}
{a : α}
{b : α}
{l : List α}
(p : List.Chain R a (b :: l))
:
List.Chain R b l
theorem
List.Chain.imp'
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(HRS : ∀ ⦃a b : α⦄, R a b → S a b)
{a : α}
{b : α}
(Hab : ∀ ⦃c : α⦄, R a c → S b c)
{l : List α}
(p : List.Chain R a l)
:
List.Chain S b l
theorem
List.Chain.imp
{α : Type u_1}
{R : α → α → Prop}
{S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{a : α}
{l : List α}
(p : List.Chain R a l)
:
List.Chain S a l
theorem
List.Pairwise.chain :
∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, List.Pairwise R (a :: l) → List.Chain R a l
range', range #
theorem
List.chain_succ_range'
(s : Nat)
(n : Nat)
(step : Nat)
:
List.Chain (fun (a b : Nat) => b = a + step) s (List.range' (s + step) n step)
theorem
List.chain_lt_range'
(s : Nat)
(n : Nat)
{step : Nat}
(h : 0 < step)
:
List.Chain (fun (x x_1 : Nat) => x < x_1) s (List.range' (s + step) n step)
@[deprecated List.getElem_range']
theorem
List.get_range'
{n : Nat}
{m : Nat}
{step : Nat}
(i : Nat)
(H : i < (List.range' n m step).length)
:
(List.range' n m step).get ⟨i, H⟩ = n + step * i
@[deprecated List.getElem?_range]
@[deprecated List.getElem_range]
theorem
List.get_range
{n : Nat}
(i : Nat)
(H : i < (List.range n).length)
:
(List.range n).get ⟨i, H⟩ = i
indexOf and indexesOf #
theorem
List.foldrIdx_start
{α : Type u_1}
{xs : List α}
:
∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat},
List.foldrIdx f i xs s = List.foldrIdx (fun (i : Nat) => f (i + s)) i xs
@[simp]
theorem
List.foldrIdx_cons
{α : Type u_1}
{x : α}
{xs : List α}
:
∀ {α_1 : Sort u_2} {f : Nat → α → α_1 → α_1} {i : α_1} {s : Nat},
List.foldrIdx f i (x :: xs) s = f s x (List.foldrIdx f i xs (s + 1))
theorem
List.findIdxs_cons
{α : Type u_1}
{x : α}
{xs : List α}
{p : α → Bool}
:
List.findIdxs p (x :: xs) = bif p x then 0 :: List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
else List.map (fun (x : Nat) => x + 1) (List.findIdxs p xs)
theorem
List.indexesOf_cons
{α : Type u_1}
{x : α}
{xs : List α}
{y : α}
[BEq α]
:
List.indexesOf y (x :: xs) = bif x == y then 0 :: List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
else List.map (fun (x : Nat) => x + 1) (List.indexesOf y xs)
theorem
List.indexOf_mem_indexesOf
{α : Type u_1}
{x : α}
[BEq α]
[LawfulBEq α]
{xs : List α}
(m : x ∈ xs)
:
List.indexOf x xs ∈ List.indexesOf x xs
insertP #
theorem
List.insertP_loop
{α : Type u_1}
{p : α → Bool}
(a : α)
(l : List α)
(r : List α)
:
List.insertP.loop p a l r = r.reverseAux (List.insertP p a l)
@[simp]
@[simp]
theorem
List.insertP_cons_neg
{α : Type u_1}
(p : α → Bool)
(a : α)
(b : α)
(l : List α)
(h : ¬p b = true)
:
List.insertP p a (b :: l) = b :: List.insertP p a l
@[simp]
theorem
List.length_insertP
{α : Type u_1}
(p : α → Bool)
(a : α)
(l : List α)
:
(List.insertP p a l).length = l.length + 1
@[simp]
theorem
List.merge_loop_nil_left
{α : Type u_1}
(s : α → α → Bool)
(r : List α)
(t : List α)
:
List.merge.loop s [] r t = t.reverseAux r
merge #
theorem
List.merge_loop_nil_right
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(t : List α)
:
List.merge.loop s l [] t = t.reverseAux l
theorem
List.merge_loop
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(r : List α)
(t : List α)
:
List.merge.loop s l r t = t.reverseAux (List.merge s l r)
@[simp]
@[simp]
theorem
List.cons_merge_cons
{α : Type u_1}
(s : α → α → Bool)
(a : α)
(b : α)
(l : List α)
(r : List α)
:
List.merge s (a :: l) (b :: r) = if s a b = true then a :: List.merge s l (b :: r) else b :: List.merge s (a :: l) r
@[simp]
theorem
List.cons_merge_cons_pos
{α : Type u_1}
{a : α}
{b : α}
(s : α → α → Bool)
(l : List α)
(r : List α)
(h : s a b = true)
:
List.merge s (a :: l) (b :: r) = a :: List.merge s l (b :: r)
@[simp, irreducible]
theorem
List.length_merge
{α : Type u_1}
(s : α → α → Bool)
(l : List α)
(r : List α)
:
(List.merge s l r).length = l.length + r.length
theorem
List.mem_merge_left
{α : Type u_1}
{x : α}
{l : List α}
{r : List α}
(s : α → α → Bool)
(h : x ∈ l)
:
x ∈ List.merge s l r
theorem
List.mem_merge_right
{α : Type u_1}
{x : α}
{r : List α}
{l : List α}
(s : α → α → Bool)
(h : x ∈ r)
:
x ∈ List.merge s l r
foldlM and foldrM #
theorem
List.foldlM_map
{m : Type u_1 → Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{α : Type u_1}
[Monad m]
(f : β₁ → β₂)
(g : α → β₂ → m α)
(l : List β₁)
(init : α)
:
List.foldlM g init (List.map f l) = List.foldlM (fun (x : α) (y : β₁) => g x (f y)) init l
theorem
List.foldrM_map
{m : Type u_1 → Type u_2}
{β₁ : Type u_3}
{β₂ : Type u_4}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(f : β₁ → β₂)
(g : β₂ → α → m α)
(l : List β₁)
(init : α)
:
List.foldrM g init (List.map f l) = List.foldrM (fun (x : β₁) (y : α) => g (f x) y) init l