An Any f p is a predicate testing a collection as :: f a for the fact that at least one item in as satisfies p. Represents the "exists" quantifier over a given universe.

This is mostly useful for its Decidable and TFunctor instances, which lets you lift predicates on p to predicates on Any f p.

A WitAny p as is a witness that, for at least one item a in the type-level collection as, the predicate p a is true.

A None f p is a predicate on a collection as that no a in as satisfies predicate p.

It is impossible for any value in a collection to be Impossible.

Since: 0.1.2.0

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if any item in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests existential quantification.

decideAny, but providing an Elem.

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if no item in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

decideNone, but providing an Elem.

If there exists an a s.t. p a, and if p implies q, then there must exist an a s.t. q a.

entailAny, but providing an Elem.

If p implies q under some context h, and if there exists some a such that p a, then there must exist some a such that p q under that context h.

h might be something like, say, Maybe, to give predicate that is either provably true or unprovably false.

Note that it is not possible to do this with p a -> Decision (q a). This is if the p a -> Decision (q a) implication is false, there it doesn't mean that there is no a such that q a, necessarily. There could have been an a where p does not hold, but q does.

entailAnyF, but providing an Elem.

An All f p is a predicate testing a collection as :: f a for the fact that all items in as satisfy p. Represents the "forall" quantifier over a given universe.

This is mostly useful for its Decidable, Provable, and TFunctor instances, which lets you lift predicates on p to predicates on All f p.

A WitAll p as is a witness that the predicate p a is true for all items a in the type-level collection as.

A NotAll f p is a predicate on a collection as that at least one a in as does not satisfy predicate p.

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if all items in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests universal quantification.

decideAll, but providing an Elem.

If for all a we have p a, and if p implies q, then for all a we must also have p a.

entailAll, but providing an Elem.

If p implies q under some context h, and if we have p a for all a, then we must have q a for all a under context h.

entailAllF, but providing an Elem.

If we have p a for all a, and p a can be used to test for q a, then we can test all as for q a.

entailAllF, but providing an Elem.

If something is true for all xs, then it must be true for at least one x in xs, provided that xs is not empty.

Since: 0.1.5.0

If p is false for all a in as, then no a in as satisfies p.

Since: 0.1.2.0

If no a in as satisfies p, then p is false for all a in as. Requires Decidable p to interrogate the input disproof.

Since: 0.1.2.0

If any a in as does not satisfy p, then not all a in as satisfy p.

Since: 0.1.2.0

If not all a in as satisfy p, then there must be at least one a in as that does not satisfy p. Requires Decidable p in order to locate that specific a.

Since: 0.1.2.0