		Search-engine friendly clone of the ACL2 documentation.

Custom-transform-hooks

Vl-design-constcheck-hook

Beta transform, not ready for public release.

Definitions and Theorems

Theorem: vl-design-p-of-vl-design-constcheck-hook

(defthm vl-design-p-of-vl-design-constcheck-hook
        (vl-design-p (vl-design-constcheck-hook x limit)))

Function: vl-design-constcheck-hook-default

(defun vl-design-constcheck-hook-default
       (x limit)
       (declare (xargs :guard (and (vl-design-p x) (natp limit)))
                (ignorable limit))
       (vl-design-fix x))