Major Section: ACL2-BUILT-INS
Oracle-funcall evaluates its first argument to produce an ACL2 function
symbol, and then applies that function symbol to the values of the rest of
the arguments. The return value is of the form (mv call-result state).
Examples: (oracle-funcall 'cons 3 4) ==> (mv '(3 . 4) <state>) (oracle-funcall (car '(floor foo bar)) (+ 6 7) 5) ==> (mv 2 <state>)
Oracle-funcall is a macro; each of its calls macroexpands to a call of
the related utility oracle-apply that takes the ACL2 state as an
argument, as follows:
(oracle-funcall fn x1 x2 .. xk)macroexpands to
(oracle-apply fn (list x1 x2 .. xk) state)
Note that calls of oracle-funcall and oracle-apply return two values:
the result of the function application, and a modified state.
See oracle-apply for details, including information about guards.
