@[implemented_by _private.Init.Data.Array.Attach.0.Array.attachWithImpl]

def Array.attachWith {α : Type u_1} (xs : Array α) (P : α → Prop) (H : ∀ (x : α), x ∈ xs → P x) : Array { x : α // P x }

O(1). "Attach" a proof P x that holds for all the elements of xs to produce a new array with the same elements but in the type {x // P x}.

Equations

• xs.attachWith P H = { data := xs.data.attachWith P ⋯ }

@[inline]

def Array.attach {α : Type u_1} (xs : Array α) : Array { x : α // x ∈ xs }

O(1). "Attach" the proof that the elements of xs are in xs to produce a new array with the same elements but in the type {x // x ∈ xs}.

Equations

• xs.attach = xs.attachWith (Membership.mem xs) ⋯