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