1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
\DOC dest_iff
\TYPE {dest_iff : term -> term * term}
\SYNOPSIS
Term destructor for logical equivalence.
\DESCRIBE
{dest_iff(`t1 <=> t2`)} returns {(`t1`,`t2`)}.
\FAILURE
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.
\SEEALSO
dest_eq, is_iff, mk_iff.
\ENDDOC
|
