mk_iff : term * term -> term
Constructs a logical equivalence (Boolean equation).
mk_iff(`t1`,`t2`) returns `t1 <=> t2`.
- FAILURE CONDITIONS
Fails with unless t1 and t2 both have Boolean type.
# mk_iff(`x = 1`,`1 = x`);;
val it : term = `x = 1 <=> 1 = x`
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