is_eq
boolSyntax.is_eq : term -> bool
Tests a term to see if it is an equation.
If M has the form t1 = t2 then is_eq M returns true. If M is not an equation the result is false.
M
t1 = t2
is_eq M
true
false
Never fails.
boolSyntax.mk_eq, boolSyntax.dest_eq
boolSyntax.mk_eq
boolSyntax.dest_eq