Macro to prove and record secondary input and output types of an ACL2 function.
This has to be used on the functions of interest
(i.e. functions for which we want to generate Java code)
prior to calling ATJ,
so that ATJ can take advantage of the type information
recorded for the functions.
This is only relevant
when
Each of the successful calls of this macro will result in an overloaded method with the specified types.