Lemmas about Vector.findSome?
, Vector.find?
, Vector.findFinIdx?
. #
We are still missing results about idxOf?
, findIdx
, and findIdx?
.
findSome? #
@[simp]
@[reducible, inline, deprecated Vector.findSome?_replicate_of_isSome (since := "2025-03-18")]
abbrev
Vector.findSome?_mkVector_of_isSome
{α✝ : Type u_1}
{α✝¹ : Type u_2}
{f : α✝ → Option α✝¹}
{n : Nat}
{a : α✝}
:
Equations
Instances For
find? #
theorem
Vector.find?_eq_some_iff_append
{α : Type}
{n : Nat}
{p : α → Bool}
{b : α}
{xs : Vector α n}
:
findFinIdx? #
theorem
Vector.findFinIdx?_push
{α : Type u_1}
{n : Nat}
{xs : Vector α n}
{a : α}
{p : α → Bool}
:
findFinIdx? p (xs.push a) = (Option.map Fin.castSucc (findFinIdx? p xs)).or (if p a = true then some ⟨n, ⋯⟩ else none)
theorem
Vector.findFinIdx?_append
{α : Type u_1}
{n₁ n₂ : Nat}
{xs : Vector α n₁}
{ys : Vector α n₂}
{p : α → Bool}
:
findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or (Option.map (Fin.natAdd n₁) (findFinIdx? p ys))
@[simp]