		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-function

Signature
(trans-function val state) → *

Definitions and Theorems

Function: trans-function

(defun trans-function (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-function))
    (declare (ignorable acl2::__function__))
    (b* (((unless (and (true-listp val) (consp val)))
          val)
         ((list* first second rest) val)
         (new-second (trans-func-option first second state))
         (new-functions (cons first
                              (cons new-second
                                    (trans-function rest state)))))
      new-functions)))