An ACL2 evaluator that returns state
(trans-eval-state form ctx state)
where form is a form to evaluate, ctx is a context (see ctx), and state is the ACL2 state. After form is (translated to
internal form and) evaluated, the new ACL2 state is returned. See trans-eval-error-triple for a potentially more useful version of this
function that returns an error-triple, which provides an error and
value as well rather than just a new state.