forAll package:what4

Expressions appearing in the problem as existentially quantified when the problem is expressed in negation normal form. This is a map from the existential quantifier element to the info.

forallPred sym v e returns an expression that represents forall v . e. Throws a user error if bound var has already been used in a quantifier.

forall_ vars t denotes a predicate that holds if t for every valuation of the variables in vars.

Create a forall expression

Indicates whether the problem needs exists-forall support.