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}
.