strip_ncomb : int -> term -> term * term list

SYNOPSIS
Strip away a given number of arguments from a combination.

DESCRIPTION
Given a number n and a combination term `f a1 ... an`, the function strip_ncomb returns the result of stripping away exactly n arguments: the pair `f`,[`a1`;...;`an`]. Note that exactly n arguments are stripped even if f is a combination.

FAILURE CONDITIONS
Fails if there are not n arguments to strip off.

EXAMPLE
Note how the behaviour is more limited compared with simple strip_comb:
  # strip_ncomb 2 `f u v x y z`;;
  Warning: inventing type variables
  val it : term * term list = (`f u v x`, [`y`; `z`])

  # strip_comb `f u v x y z`;;
  Warning: inventing type variables
  val it : term * term list = (`f`, [`u`; `v`; `x`; `y`; `z`])

USES
Delicate term decompositions.

SEE ALSO
strip_comb.