ADD-RAW-ARITY

add arity information for raw mode 
Major Section:  SET-RAW-MODE

Users of raw mode (see set-raw-mode) can use arbitrary raw Lisp functions that are not known inside the usual ACL2 loop. In such cases, ACL2 may not know how to display multiple values returned by ACL2's mv macro. The following example should make this clear. 

ACL2 P>(defun foo (x y) (mv y x))
FOO
ACL2 P>(foo 3 4)


Note: Unable to compute number of values returned by this evaluation
because function FOO is not known in the ACL2 logical world.  Presumably
it was defined in raw Lisp or in raw mode.  Returning the first (perhaps
only) value for calls of FOO.
4
ACL2 P>(add-raw-arity foo 2)
 RAW-ARITY-ALIST
ACL2 P>(foo 3 4)
(4 3)
ACL2 P>
The first argument of add-raw-arity should be a symbol, representing the name of a function, macro, or special form, and the second argument should either be a non-negative integer (denoting the number of values returned by ACL2) or else the symbol :LAST, meaning that the number of values returned by the call is the number of values returned by the last argument.

The current arity assignments can be seen by evaluating (@ raw-arity-alist). See remove-raw-arity for how to undo a call of add-raw-arity.