dest_iff : term -> term * term
Term destructor for logical equivalence.
dest_iff(`t1 <=> t2`) returns (`t1`,`t2`).
- FAILURE CONDITIONS
Fails with if term is not a logical equivalence, i.e. an equation between terms
of Boolean type.
# dest_iff `x = y <=> y = 1`;;
val it : term * term = (`x = y`, `y = 1`)
The function dest_eq has the same effect, but the present function checks
that the types of the two sides are indeed Boolean, whereas dest_eq will
break apart any equation.
- SEE ALSO
dest_eq, is_iff, mk_iff.