strip_binder
Term.strip_binder : term option -> term -> term list * term
Break apart consecutive binders.
An application strip_binder (SOME c) (c(\v1. ... (c(\vn.M))...))
returns ([v1,...,vn],M). The constant c should represent a term
binding operation.
An application strip_binder NONE (\v1...vn. M) returns
([v1,...,vn],M).
Failure
Never fails.
Example
strip_abs could be defined as follows.
- val strip_abs = strip_binder NONE;
> val strip_abs = fn : term -> term list * term
- strip_abs (Term `\x y z. x /\ y ==> z`);
> val it = ([`x`, `y`, `z`], `x /\ y ==> z`) : term list * term
Defining strip_forall is similar.
strip_binder (SOME boolSyntax.universal)
Comments
Terms with many consecutive binders should be taken apart using
strip_binder and its instantiations strip_abs, strip_forall, and
strip_exists. In the current implementation of HOL, iterating
dest_abs, dest_forall, or dest_exists is far slower for terms with
many consecutive binders.
See also
Term.list_mk_binder,
Term.strip_abs,
boolSyntax.strip_forall,
boolSyntax.strip_exists