		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-argument

Signature
(trans-argument val state) → *

Definitions and Theorems

Function: trans-argument

(defun trans-argument (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-argument))
    (declare (ignorable acl2::__function__))
    (b* (((unless (and (true-listp val)
                       (car val)
                       (cadr val)))
          val)
         ((list* name type rest) val)
         (to-be-trans (cons type (cons name 'nil)))
         ((mv err term)
          (acl2::translate-cmp
               to-be-trans t t nil
               'smtlink-process-user-hint->trans-hypothesis
               (w state)
               (default-state-vars t)))
         ((when err)
          (er hard?
              'smtlink-process-user-hint->trans-argument
              "Error ~
    translating form: ~q0"
              to-be-trans)))
      (cons name (cons (car term) rest)))))