Documentation

Batteries.Data.List.Init.Attach

def List.pmap {α : Type u_1} {β : Type u_2} {P : αProp} (f : (a : α) → P aβ) (l : List α) (H : ∀ (a : α), a lP 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
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 lP 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
Instances For
@[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)
Instances For