Major Section: SET-RAW-MODE
Technical note: This macro is a no-op, and is not necessary, when ACL2 is built with #-acl2-mv-as-values.
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 a multiple value 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.
