toArray #
next? #
dropLast #
set #
theorem
List.set_eq_modify
{α : Type u_1}
(a : α)
(n : Nat)
(l : List α)
:
l.set n a = List.modify (fun (x : α) => a) n l
theorem
List.modify_eq_set_get?
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modify f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l
theorem
List.modify_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
List.modify f n l = l.set n (f (l.get ⟨n, h⟩))
tail #
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.toList ++ xs → List.extractP.go p l xs acc = (List.find? p xs, acc.toList ++ List.eraseP p xs)
erase #
findIdx? #
theorem
List.findIdx_eq_findIdx?
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
List.findIdx p l = match List.findIdx? p l with
| some i => i
| none => l.length
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 #
theorem
List.disjoint_of_subset_left
{α✝ : Type u_1}
{l₁ l l₂ : List α✝}
(ss : l₁ ⊆ l)
(d : l.Disjoint l₂)
:
l₁.Disjoint l₂
theorem
List.disjoint_of_subset_right
{α✝ : Type u_1}
{l₂ l l₁ : List α✝}
(ss : l₂ ⊆ l)
(d : l₁.Disjoint l)
:
l₁.Disjoint l₂
theorem
List.disjoint_of_disjoint_cons_left
{α✝ : Type u_1}
{a : α✝}
{l₁ l₂ : List α✝}
:
(a :: l₁).Disjoint l₂ → l₁.Disjoint l₂
theorem
List.disjoint_of_disjoint_cons_right
{α✝ : Type u_1}
{a : α✝}
{l₁ l₂ : List α✝}
:
l₁.Disjoint (a :: l₂) → l₁.Disjoint l₂
theorem
List.disjoint_of_disjoint_append_left_left
{α✝ : Type u_1}
{l₁ l₂ l : List α✝}
(d : (l₁ ++ l₂).Disjoint l)
:
l₁.Disjoint l
theorem
List.disjoint_of_disjoint_append_left_right
{α✝ : Type u_1}
{l₁ l₂ l : List α✝}
(d : (l₁ ++ l₂).Disjoint l)
:
l₂.Disjoint l
theorem
List.disjoint_of_disjoint_append_right_left
{α✝ : Type u_1}
{l l₁ l₂ : List α✝}
(d : l.Disjoint (l₁ ++ l₂))
:
l.Disjoint l₁
theorem
List.disjoint_of_disjoint_append_right_right
{α✝ : Type u_1}
{l l₁ l₂ : List α✝}
(d : l.Disjoint (l₁ ++ l₂))
:
l.Disjoint l₂
union #
theorem
List.union_def
{α : Type u_1}
[BEq α]
(l₁ l₂ : List α)
:
l₁ ∪ l₂ = List.foldr List.insert l₂ l₁
@[simp]
theorem
List.cons_union
{α : Type u_1}
[BEq α]
(a : α)
(l₁ l₂ : List α)
:
a :: l₁ ∪ l₂ = List.insert a (l₁ ∪ l₂)
inter #
theorem
List.inter_def
{α : Type u_1}
[BEq α]
(l₁ 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₁ 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 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 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 α✝}
(p : List.Pairwise R (a :: l))
:
List.Chain R a l
range', range #
theorem
List.chain_succ_range'
(s n step : Nat)
:
List.Chain (fun (a b : Nat) => b = a + step) s (List.range' (s + step) n step)
theorem
List.chain_lt_range'
(s n : Nat)
{step : Nat}
(h : 0 < step)
:
List.Chain (fun (x1 x2 : Nat) => x1 < x2) s (List.range' (s + step) n step)
@[deprecated List.getElem?_range']
theorem
List.get?_range'
(s step : Nat)
{m n : Nat}
(h : m < n)
:
(List.range' s n step).get? m = some (s + step * m)
@[deprecated List.getElem_range']
theorem
List.get_range'
{n m 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 α}
{α✝ : Sort u_2}
{f : Nat → α → α✝ → α✝}
{i : α✝}
{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 α}
{α✝ : Sort u_2}
{f : Nat → α → α✝ → α✝}
{i : α✝}
{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)
@[simp]
theorem
List.eraseIdx_indexOf_eq_erase
{α : Type u_1}
[BEq α]
(a : α)
(l : List α)
:
l.eraseIdx (List.indexOf a l) = l.erase a
theorem
List.indexOf_mem_indexesOf
{α : Type u_1}
{x : α}
[BEq α]
[LawfulBEq α]
{xs : List α}
(m : x ∈ xs)
:
List.indexOf x xs ∈ List.indexesOf x xs
theorem
List.indexOf?_cons
{α : Type u_1}
{x : α}
{xs : List α}
{y : α}
[BEq α]
:
List.indexOf? y (x :: xs) = if (x == y) = true then some 0 else Option.map Nat.succ (List.indexOf? y xs)
theorem
List.indexOf_eq_indexOf?
{α : Type u_1}
[BEq α]
(a : α)
(l : List α)
:
List.indexOf a l = match List.indexOf? a l with
| some i => i
| none => l.length
insertP #
theorem
List.insertP_loop
{α : Type u_1}
{p : α → Bool}
(a : α)
(l 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]
deprecations #
@[deprecated List.isEmpty_iff]
Alias of List.isEmpty_iff.
@[deprecated List.modify_nil]
Alias of List.modify_nil.
@[deprecated List.modify_zero_cons]
theorem
List.modifyNth_zero_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
:
List.modify f 0 (a :: l) = f a :: l
Alias of List.modify_zero_cons.
@[deprecated List.modify_succ_cons]
theorem
List.modifyNth_succ_cons
{α : Type u_1}
(f : α → α)
(a : α)
(l : List α)
(n : Nat)
:
List.modify f (n + 1) (a :: l) = a :: List.modify f n l
Alias of List.modify_succ_cons.
@[deprecated List.modifyTailIdx_id]
Alias of List.modifyTailIdx_id.
@[deprecated List.eraseIdx_eq_modifyTailIdx]
theorem
List.eraseIdx_eq_modifyNthTail
{α : Type u_1}
(n : Nat)
(l : List α)
:
l.eraseIdx n = List.modifyTailIdx List.tail n l
Alias of List.eraseIdx_eq_modifyTailIdx.
@[deprecated List.getElem?_modify]
theorem
List.getElem?_modifyNth
{α : 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]?
Alias of List.getElem?_modify.
@[deprecated List.getElem?_modify]
theorem
List.get?_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
(m : Nat)
:
(List.modify f n l).get? m = (fun (a : α) => if n = m then f a else a) <$> l.get? m
@[deprecated List.length_modifyTailIdx]
theorem
List.length_modifyNthTail
{α : Type u_1}
(f : List α → List α)
(H : ∀ (l : List α), (f l).length = l.length)
(n : Nat)
(l : List α)
:
(List.modifyTailIdx f n l).length = l.length
Alias of List.length_modifyTailIdx.
@[deprecated List.length_modifyTailIdx]
theorem
List.modifyNthTail_length
{α : Type u_1}
(f : List α → List α)
(H : ∀ (l : List α), (f l).length = l.length)
(n : Nat)
(l : List α)
:
(List.modifyTailIdx f n l).length = l.length
Alias of List.length_modifyTailIdx.
@[deprecated List.modifyTailIdx_add]
theorem
List.modifyNthTail_add
{α : Type u_1}
(f : List α → List α)
(n : Nat)
(l₁ l₂ : List α)
:
List.modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ List.modifyTailIdx f n l₂
Alias of List.modifyTailIdx_add.
@[deprecated List.exists_of_modifyTailIdx]
theorem
List.exists_of_modifyNthTail
{α : Type u_1}
(f : List α → List α)
{n : Nat}
{l : List α}
(h : n ≤ l.length)
:
Alias of List.exists_of_modifyTailIdx.
@[deprecated List.length_modify]
theorem
List.length_modifyNth
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l).length = l.length
Alias of List.length_modify.
@[deprecated List.length_modify]
theorem
List.modifyNth_get?_length
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l).length = l.length
Alias of List.length_modify.
@[deprecated List.getElem?_modify_eq]
theorem
List.getElem?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l)[n]? = f <$> l[n]?
Alias of List.getElem?_modify_eq.
@[deprecated List.getElem?_modify_eq]
theorem
List.get?_modifyNth_eq
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
(List.modify f n l).get? n = f <$> l.get? n
@[deprecated List.getElem?_modify_ne]
theorem
List.getElem?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modify f m l)[n]? = l[n]?
Alias of List.getElem?_modify_ne.
@[deprecated List.getElem?_modify_ne]
theorem
List.get?_modifyNth_ne
{α : Type u_1}
(f : α → α)
{m n : Nat}
(l : List α)
(h : m ≠ n)
:
(List.modify f m l).get? n = l.get? n
@[deprecated List.modifyTailIdx_eq_take_drop]
theorem
List.modifyNthTail_eq_take_drop
{α : Type u_1}
(f : List α → List α)
(H : f [] = [])
(n : Nat)
(l : List α)
:
List.modifyTailIdx f n l = List.take n l ++ f (List.drop n l)
Alias of List.modifyTailIdx_eq_take_drop.
@[deprecated List.modify_eq_take_drop]
theorem
List.modifyNth_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)
Alias of List.modify_eq_take_drop.
@[deprecated List.modify_eq_take_cons_drop]
theorem
List.modifyNth_eq_take_cons_drop
{α : Type u_1}
{f : α → α}
{n : Nat}
{l : List α}
(h : n < l.length)
:
Alias of List.modify_eq_take_cons_drop.
@[deprecated List.set_eq_modify]
theorem
List.set_eq_modifyNth
{α : Type u_1}
(a : α)
(n : Nat)
(l : List α)
:
l.set n a = List.modify (fun (x : α) => a) n l
Alias of List.set_eq_modify.
@[deprecated List.modify_eq_set_get?]
theorem
List.modifyNth_eq_set_get?
{α : Type u_1}
(f : α → α)
(n : Nat)
(l : List α)
:
List.modify f n l = ((fun (a : α) => l.set n (f a)) <$> l.get? n).getD l
Alias of List.modify_eq_set_get?.
@[deprecated List.modify_eq_set_get]
theorem
List.modifyNth_eq_set_get
{α : Type u_1}
(f : α → α)
{n : Nat}
{l : List α}
(h : n < l.length)
:
List.modify f n l = l.set n (f (l.get ⟨n, h⟩))
Alias of List.modify_eq_set_get.