dest_imp : term -> term * term
SYNOPSIS
Breaks apart an implication into antecedent and consequent.
DESCRIPTION
dest_imp
is a term destructor for implications. Thus
dest_imp `t1 ==> t2`
returns
(`t1`,`t2`)
FAILURE CONDITIONS
Fails with
dest_imp
if term is not an implication.
COMMENTS
Previous version of
dest_imp
treats negations as an implication with
F
as the conclusion. This is renamed to
dest_neg_imp
.
SEE ALSO
mk_imp
,
is_imp
,
strip_imp
,
dest_neg_imp
.