Properties of List.enum

theorem List.get?_enumFrom {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) : (List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)

@[deprecated List.get?_enumFrom]

theorem List.enumFrom_get? {α : Type u_1} (n : ℕ) (l : List α) (m : ℕ) : (List.enumFrom n l).get? m = Option.map (fun (a : α) => (n + m, a)) (l.get? m)

Alias of List.get?_enumFrom.

theorem List.get?_enum {α : Type u_1} (l : List α) (n : ℕ) : l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)

@[deprecated List.get?_enum]

theorem List.enum_get? {α : Type u_1} (l : List α) (n : ℕ) : l.enum.get? n = Option.map (fun (a : α) => (n, a)) (l.get? n)

Alias of List.get?_enum.

theorem List.get_enumFrom {α : Type u_1} (l : List α) (n : ℕ) (i : Fin (List.enumFrom n l).length) : (List.enumFrom n l).get i = (n + ↑i, l.get (Fin.cast ⋯ i))

theorem List.get_enum {α : Type u_1} (l : List α) (i : Fin l.enum.length) : l.enum.get i = (↑i, l.get (Fin.cast ⋯ i))

@[deprecated List.mk_add_mem_enumFrom_iff_getElem?]

theorem List.mk_add_mem_enumFrom_iff_get? {α : Type u_1} {n : ℕ} {i : ℕ} {x : α} {l : List α} : (n + i, x) ∈ List.enumFrom n l ↔ l.get? i = some x

@[deprecated List.mk_mem_enumFrom_iff_le_and_getElem?_sub]

theorem List.mk_mem_enumFrom_iff_le_and_get?_sub {α : Type u_1} {n : ℕ} {i : ℕ} {x : α} {l : List α} : (i, x) ∈ List.enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = some x

@[deprecated List.mem_enum_iff_getElem?]

theorem List.mk_mem_enum_iff_get? {α : Type u_1} {i : ℕ} {x : α} {l : List α} : (i, x) ∈ l.enum ↔ l.get? i = some x

@[deprecated List.mk_mem_enum_iff_getElem?]

theorem List.mem_enum_iff_get? {α : Type u_1} {x : ℕ × α} {l : List α} : x ∈ l.enum ↔ l.get? x.fst = some x.snd