dest_iff : term -> term * term
- SYNOPSIS
-
Term destructor for logical equivalence.
- DESCRIPTION
-
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.
- EXAMPLE
-
# dest_iff `x = y <=> y = 1`;;
val it : term * term = (`x = y`, `y = 1`)
- COMMENTS
-
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.