		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-functions

Signature
(trans-functions val state) → *

Definitions and Theorems

Function: trans-functions

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