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.

Equations

• List.pmap f [] x_2 = []
• List.pmap f (a :: l) H = f a ⋯ :: List.pmap f l ⋯

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

Equations

• l.attachWith P H = List.pmap Subtype.mk l H

@[inline]

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

O(1). "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

• l.attach = l.attachWith (fun (x : α) => x ∈ l) ⋯