		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))