Idris2Doc : Data.List.Quantifiers

Data.List.Quantifiers

allNegAny : All (Not.p) xs -> Not (Anypxs)
  If none of the elements satisfy the property, then not any single one can.

Totality: total
anyNegAll : Any (Not.p) xs -> Not (Allpxs)
  If there exists an element that doesn't satify the property, then it is
not the case that all elements satisfy it.

Totality: total
indexAll : Elemxxs -> Allpxs -> px
  Given a proof of membership for some element, extract the property proof for it

Totality: total
negAnyAll : Not (Anypxs) -> All (Not.p) xs
  If there does not exist an element that satifies the property, then it is
the case that all elements do not satisfy it.

Totality: total
pullOut : List (Subsetap) -> Subset (Lista) (Allp)
  Pull the elementwise property out to the list level

Totality: total
pushIn : (xs : Lista) -> (0 _ : Allpxs) -> List (Subsetap)
  Push in the property from the list level with element level

Totality: total
pushInOutInverse : (xs : Lista) -> (0 prf : Allpxs) -> pullOut (pushInxsprf) = Elementxsprf
Totality: total
pushOutInInverse : (xs : List (Subsetap)) -> uncurrypushIn (pullOutxs) = xs
Totality: total