		Search-engine friendly clone of the ACL2 documentation.

2vec

2vec->val

Extract the upper/lower value (both the same) from a 2vec.

Signature
(2vec->val x) → *
Arguments: x — Guard (and (4vec-p x) (2vec-p x)).

Definitions and Theorems

Function: 2vec->val$inline

(defun 2vec->val$inline (x)
  (declare (xargs :guard (and (4vec-p x) (2vec-p x))))
  (let ((__function__ '2vec->val))
    (declare (ignorable __function__))
    (mbe :logic (4vec->upper x) :exec x)))