Documentation

Init.Data.Array.Attach

@[implemented_by _private.Init.Data.Array.Attach.0.Array.attachWithImpl]
def Array.attachWith {α : Type u_1} (xs : Array α) (P : αProp) (H : ∀ (x : α), x xsP x) :
Array { x : α // P x }

O(1). "Attach" a proof P x that holds for all the elements of xs to produce a new array with the same elements but in the type {x // P x}.

Equations
  • xs.attachWith P H = { data := xs.data.attachWith P }
Instances For
    @[inline]
    def Array.attach {α : Type u_1} (xs : Array α) :
    Array { x : α // x xs }

    O(1). "Attach" the proof that the elements of xs are in xs to produce a new array with the same elements but in the type {x // x ∈ xs}.

    Equations
    • xs.attach = xs.attachWith (fun (x : α) => x xs)
    Instances For