		Search-engine friendly clone of the ACL2 documentation.

Exec-fun

Execute a function on argument values.

Signature
(exec-fun fun args compst fenv limit) → (mv result new-compst)
Arguments: fun — Guard (identp fun).; args — Guard (value-listp args).; compst — Guard (compustatep compst).; fenv — Guard (fun-envp fenv).; limit — Guard (natp limit).
Returns: result — Type (value-option-resultp result).; new-compst — Type (compustatep new-compst).

We retrieve the information about the function from the environment. We initialize a scope with the argument values, and we push a frame onto the call stack. We execute the function body, which must return a result that matches the function's result type. We pop the frame and return the value of the function call as result.