is_imp
boolSyntax.is_imp : term -> bool
Tests a term to see if it is an implication or a negation.
If M has the form t1 ==> t2, or the form ~t, then is_imp M
returns true. If the term is neither an implication nor a negation the
result is false.
Failure
Never fails.
Comments
Yields true of negations because dest_imp destructs negations (for
backwards compatibility with PPLAMBDA). Use is_imp_only if you don't
want this behaviour.
See also
boolSyntax.mk_imp,
boolSyntax.dest_imp,
boolSyntax.is_imp_only,
boolSyntax.dest_imp_only