		Search-engine friendly clone of the ACL2 documentation.

Structures

Evex->vl/rc

Get the vl/rc field of evex-prefixes.

Signature
(evex->vl/rc evex-prefixes) → vl/rc
Arguments: evex-prefixes — Guard (evex-prefixes-p evex-prefixes).
Returns: vl/rc — Type (unsigned-byte-p 2 vl/rc), given the guard.

Definitions and Theorems

Function: evex->vl/rc$inline

(defun evex->vl/rc$inline (evex-prefixes)
  (declare (xargs :guard (evex-prefixes-p evex-prefixes)))
  (evex-byte3->vl/rc (evex-prefixes->byte3 evex-prefixes)))

Theorem: return-type-of-evex->vl/rc

(defthm return-type-of-evex->vl/rc
  (implies (and (evex-prefixes-p$inline evex-prefixes))
           (b* ((vl/rc (evex->vl/rc$inline evex-prefixes)))
             (unsigned-byte-p 2 vl/rc)))
  :rule-classes :rewrite)