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

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.

Equations

• List.pmap f [] x_2 = []
• List.pmap f (a :: l) H = f a (_ : p a) :: List.pmap f l (_ : ∀ (x : α), x ∈ l → p x)

@[implemented_by _private.Std.Data.List.Init.Attach.0.List.attachImpl]

def List.attach {α : Type u_1} (l : List α) : List { x : α // x ∈ l }

"Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

Equations

• List.attach l = List.pmap Subtype.mk l (_ : ∀ (x : α), x ∈ l → x ∈ l)