mk_forall

boolSyntax.mk_forall : term * term -> term

Term constructor for universal quantification.

If v is a variable and t is a term of type bool, then mk_forall (v,t) returns the term !v. t.

Failure

Fails if v is not a variable or if t is not of type bool.

See also

boolSyntax.dest_forall, boolSyntax.is_forall, boolSyntax.list_mk_forall, boolSyntax.strip_forall