dest_eq_ty
boolSyntax.dest_eq_ty : term -> term * term * hol_type
Term destructor for equality.
If M is the term t1 = t2, then dest_eq_ty M returns
(t1, t2, ty), where ty is the type of t1 (and thus also of t2).
Failure
Fails if M is not an equality.
Gives an efficient way to break apart an equality and get the type of the equality. Useful for obtaining that last fraction of speed when optimizing the bejeesus out of an inference rule.
See also
boolSyntax.mk_eq,
boolSyntax.is_eq,
boolSyntax.lhs, boolSyntax.rhs