strip_comb

boolSyntax.strip_comb : term -> term * term list

Iteratively breaks apart combinations (function applications).

If M has the form t t1 ... tn then strip_comb M returns (t,[t1,...,tn]). Note that

   strip_comb(list_mk_comb(t,[t1,...,tn]))

will not be (t,[t1,...,tn]) if t is a combination.

Failure

Never fails.

Example

- strip_comb (Term `x /\ y`);
> val it = (`$/\`, [`x`, `y`]) : term * term list

- strip_comb T;
> val it = (`T`, []) : term * term list

See also

Term.list_mk_comb, Term.dest_comb