		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-hint

Signature
(trans-hint hint state) → *

Definitions and Theorems

Function: trans-hint

(defun trans-hint (hint state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'trans-hint))
   (declare (ignorable acl2::__function__))
   (b* (((unless (true-listp hint)) hint)
        (wrld-len (wrld-fn-len state))
        ((if (atom hint))
         (cons ':wrld-len (cons wrld-len 'nil)))
        ((unless (cdr hint)) hint)
        ((list* first second rest) hint)
        (new-second (trans-hint-option first second state))
        (new-hint (cons first
                        (cons new-second (trans-hint rest state)))))
     new-hint)))