dest_comb

Term.dest_comb : term -> term * term

Breaks apart a combination (function application) into rator and rand.

dest_comb is a term destructor for combinations. If term M has the form f x, then dest_comb M equals (f,x).

Failure

Fails if the argument is not a function application.

See also

Term.mk_comb, Term.is_comb, Term.dest_var, Term.dest_const, Term.dest_abs, boolSyntax.strip_comb