def
List.pmap
{α : Type u_1}
{β : Type u_2}
{P : α → Prop}
(f : (a : α) → P a → β)
(l : List α)
(H : ∀ (a : α), a ∈ l → P a)
:

List β

`O(n)`

. Partial map. If `f : Π a, P a → β`

is a partial function defined on
`a : α`

satisfying `P`

, then `pmap f l h`

is essentially the same as `map f l`

but is defined only when all members of `l`

satisfy `P`

, using the proof
to apply `f`

.

## Instances For

@[implemented_by _private.Batteries.Data.List.Init.Attach.0.List.attachWithImpl]

def
List.attachWith
{α : Type u_1}
(l : List α)
(P : α → Prop)
(H : ∀ (x : α), x ∈ l → P x)
:

List { x : α // P x }

`O(1)`

. "Attach" a proof `P x`

that holds for all the elements of `l`

to produce a new list
with the same elements but in the type `{x // P x}`

.