		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-func-option

Signature
(trans-func-option opt val state) → *

Definitions and Theorems

Function: trans-func-option

(defun trans-func-option (opt val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-func-option))
    (declare (ignorable acl2::__function__))
    (cond ((equal opt ':formals)
           (trans-formals val state))
          ((equal opt ':returns)
           (trans-returns val state))
          ((equal opt ':guard)
           (trans-guard val state))
          ((equal opt ':more-returns)
           (trans-more-returns val state))
          (t val))))