dest_eq

boolSyntax.dest_eq : term -> term * term

Term destructor for equality.

If M is the term t1 = t2, then dest_eq M returns (t1, t2).

Failure

Fails if M is not an equality.

See also

boolSyntax.mk_eq, boolSyntax.is_eq, boolSyntax.lhs, boolSyntax.rhs