		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-hypothesis

Signature
(trans-hypothesis val state) → *

Definitions and Theorems

Function: trans-hypothesis

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