		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-hypotheses

Signature
(trans-hypotheses val state) → *

Definitions and Theorems

Function: trans-hypotheses

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