		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-formals

Signature
(trans-formals val state) → *

Definitions and Theorems

Function: trans-formals

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