mk_forall : term * term -> term

SYNOPSIS

Term constructor for universal quantification.

DESCRIPTION

mk_forall(`v`,`t`) returns `!v. t`.

FAILURE CONDITIONS

Fails with if first term is not a variable or if t is not of type `:bool`.

EXAMPLE

  # mk_forall(`x:num`,`x + 1 = 1 + x`);;
  val it : term = `!x. x + 1 = 1 + x`

SEE ALSO

dest_forall, is_forall, list_mk_forall.