Tests if a term is a binder construct with named constant.
DESCRIPTION
The call is_binder "c" t tests whether the term t has the form of an
application of a constant c to an abstraction. Note that this has nothing to
do with the parsing status of the name c as a binder, but only the form of
the term.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# is_binder "!" `!x. x >= 0`;;
val it : bool = true
Note how only the basic logical form is tested, even taking in things
that we wouldn't really think of as binders:
# is_binder "=" `(=) (\x. x + 1)`;;
val it : bool = true