		Search-engine friendly clone of the ACL2 documentation.

Translate-cmp-smtlink

Trans-guard

Signature
(trans-guard val state) → *

Definitions and Theorems

Function: trans-guard

(defun trans-guard (val state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'trans-guard))
    (declare (ignorable acl2::__function__))
    (trans-hypothesis val state)))