strip_comb : term -> term * term list

SYNOPSIS

Iteratively breaks apart combinations (function applications).

DESCRIPTION

strip_comb `t t1 ... tn` returns (`t`,[`t1`;...;`tn`]). Note that

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

will not return (`t`,[`t1`;...;`tn`]) if t is a combination.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # strip_comb `x /\ y`;;
  val it : term * term list = (`(/\)`, [`x`; `y`])

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