Checking for translator pre/side conditions.

It's common to want the top-level translated functions to not have pre-conditions or side-conditions.

The CakeML development indirectly requires this with the top-level CF theorems stated about the final toplevel declarations. If a user accidentally introduces a silly side-condition or pre-condition then the CF proof will fail. Unfortunately a lot of CPU and human work is then required to discover the problem.

Simple solution: a one-line check that a translated function doesn't (currently) have any pre-conditions or side-conditions. The CakeML development, for instance, can run this check before its final topdecls and CF proof.

If a condition is found, the error message should try to identify where in the function call graph the problematic precondition came from.