Lemmas about List.findSome?
, List.find?
, List.findIdx
, List.findIdx?
, List.idxOf
,
and List.lookup
.
findSome? #
@[reducible, inline, deprecated List.findSome?_eq_none_iff (since := "2024-09-05")]
abbrev
List.findSome?_eq_none
{α✝ : Type u_1}
{α✝¹ : Type u_2}
{p : α✝ → Option α✝¹}
{l : List α✝}
:
Equations
Instances For
@[simp]
find? #
@[reducible, inline, deprecated List.find?_eq_some_iff_append (since := "2024-11-06")]
Equations
Instances For
@[reducible, inline, deprecated List.find?_flatten_eq_none_iff (since := "2025-02-03")]
Instances For
If find? p
returns some a
from xs.flatten
, then p a
holds, and
some list in xs
contains a
, and no earlier element of that list satisfies p
.
Moreover, no earlier list in xs
has an element satisfying p
.
@[reducible, inline, deprecated List.find?_flatten_eq_some_iff (since := "2025-02-03")]
Instances For
@[reducible, inline, deprecated List.find?_replicate_eq_none_iff (since := "2025-02-03")]
Instances For
@[reducible, inline, deprecated List.find?_replicate_eq_some_iff (since := "2025-02-03")]
Instances For
findIdx? (preliminary lemmas) #
findIdx #
findIdx? #
findFinIdx? #
theorem
List.findFinIdx?_eq_pmap_findIdx?
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
findFinIdx? p xs = Option.pmap (fun (i : Nat) (m : findIdx? p xs = some i) => ⟨i, ⋯⟩) (findIdx? p xs) ⋯
theorem
List.findFinIdx?_append
{α : Type u_1}
{xs ys : List α}
{p : α → Bool}
:
findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or
(Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.length) (findFinIdx? p ys)))
@[simp]
idxOf #
The verification API for idxOf
is still incomplete.
The lemmas below should be made consistent with those for findIdx
(and proved using them).
@[reducible, inline, deprecated List.idxOf_cons (since := "2025-01-29")]
Equations
Instances For
@[reducible, inline, deprecated List.idxOf_cons_self (since := "2025-01-29")]
Equations
Instances For
@[reducible, inline, deprecated List.idxOf_append (since := "2025-01-29")]
Equations
Instances For
finIdxOf? #
The verification API for finIdxOf?
is still incomplete.
The lemmas below should be made consistent with those for findFinIdx?
(and proved using them).
idxOf? #
The verification API for idxOf?
is still incomplete.
The lemmas below should be made consistent with those for findIdx?
(and proved using them).
@[reducible, inline, deprecated List.idxOf?_eq_none_iff (since := "2025-01-29")]
Equations
Instances For
lookup #
Deprecations #
@[reducible, inline, deprecated List.find?_flatten (since := "2024-10-14")]
Equations
Instances For
@[reducible, inline, deprecated List.find?_flatten_eq_none (since := "2024-10-14")]
Instances For
@[reducible, inline, deprecated List.find?_flatten_eq_some (since := "2024-10-14")]
Instances For
@[reducible, inline, deprecated List.findIdx?_flatten (since := "2024-10-14")]