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)The first argument of
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>
add-raw-arityshould 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