Agda.TypeChecking.DropArgs

NOTE: does not work for recursive functions.

NOTE: This creates telescopes with unbound de Bruijn indices.

Use for dropping initial lambdas in clause bodies. NOTE: does not reduce term, need lambdas to be present.

To drop the first n arguments in a compiled clause, we reduce the split argument indices by n and drop n arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.