dest_imp

boolSyntax.dest_imp : term -> term * term

Breaks an implication or negation into antecedent and consequent.

dest_imp is a term destructor for implications. It treats negations as implications with consequent F. Thus, if M is a term with the form t1 ==> t2, then dest_imp M returns (t1,t2), and if M has the form ~t, then dest_imp M returns (t,F).

Failure

Fails if M is neither an implication nor a negation.

Comments

Destructs negations for increased functionality of HOL-style resolution. If the ability to destruct negations is not desired, as is only right, then use dest_imp_only.

See also

boolSyntax.mk_imp, boolSyntax.dest_imp_only, boolSyntax.is_imp, boolSyntax.is_imp_only, boolSyntax.strip_imp, boolSyntax.list_mk_imp