Trans-eval-error-triple
An ACL2 evaluator for forms that return error-triples
General Form:
(trans-eval-error-triple form ctx state)
where form is a form that evaluates to an error-triple,
ctx is a context (see ctx), and state is the ACL2 state. If form is syntactically illegal, then
(mv :trans-error :trans-error state) is returned. Otherwise,
evaluation of form should produce an error-triple (mv erp val
state), and that error-triple is returned. If you don't care about erp
or val, consider using trans-eval-state instead, which does not
require form to evaluate to an error-triple.