mk_exists : term * term -> term

SYNOPSIS

Term constructor for existential quantification.

DESCRIPTION

mk_exists(`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_exists(`x:num`,`x + 1 = 1 + x`);;
  val it : term = `?x. x + 1 = 1 + x`

SEE ALSO

dest_exists, is_exists, list_mk_exists.