list_mk_forall : term list * term -> term
- SYNOPSIS
-
Iteratively constructs a universal quantification.
- DESCRIPTION
-
list_mk_forall([`x1`;...;`xn`],`t`) returns `!x1 ... xn. t`.
- FAILURE CONDITIONS
-
Fails if any term in the list is not a variable or if t is not of type
`:bool` and the list of terms is non-empty. If the list of terms is empty the
type of t can be anything.
- EXAMPLE
-
# list_mk_forall([`x:num`; `y:num`],`x + y + 1 = SUC z`);;
val it : term = `!x y. x + y + 1 = SUC z`
- SEE ALSO
-
mk_forall, strip_forall.