mk_iff : term * term -> term

SYNOPSIS
Constructs a logical equivalence (Boolean equation).

DESCRIPTION
mk_iff(`t1`,`t2`) returns `t1 <=> t2`.

FAILURE CONDITIONS
Fails with unless t1 and t2 both have Boolean type.

EXAMPLE
  # mk_iff(`x = 1`,`1 = x`);;
  val it : term = `x = 1 <=> 1 = x`

COMMENTS
Simply mk_eq has the same effect on successful calls. However mk_iff is slightly more efficient, and will fail if the terms do not have Boolean type.

SEE ALSO
dest_iff, is_iff,mk_eq.