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.