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
30
31
|
\DOC is_eq
\TYPE {is_eq : term -> bool}
\SYNOPSIS
Tests a term to see if it is an equation.
\DESCRIBE
{is_eq `t1 = t2`} returns {true}. If the term is not an equation the result
is {false}. Note that logical equivalence is just equality on type {:bool},
even though it is printed as {<=>}.
\FAILURE
Never fails.
\EXAMPLE
{
# is_eq `2 + 2 = 4`;;
val it : bool = true
# is_eq `p /\ q <=> q /\ p`;;
val it : bool = true
# is_eq `p ==> p`;;
val it : bool = false
}
\SEEALSO
dest_eq, is_beq, mk_eq.
\ENDDOC
|
