		Search-engine friendly clone of the ACL2 documentation.

Vl-linecol

Vl-linecol->col

Signature
(vl-linecol->col x) → col
Arguments: x — Guard (vl-linecol-p x).
Returns: col — Type (natp col).

Definitions and Theorems

Function: vl-linecol->col$inline

(defun vl-linecol->col$inline (x)
  (declare (xargs :guard (vl-linecol-p x)))
  (let ((__function__ 'vl-linecol->col))
    (declare (ignorable __function__))
    (b* ((x (vl-linecol-fix x))
         ((when (consp x)) (cdr x)))
      (logand (the (unsigned-byte 52) x)
              (1- (expt 2 22))))))

Theorem: natp-of-vl-linecol->col

(defthm natp-of-vl-linecol->col
  (b* ((col (vl-linecol->col$inline x)))
    (natp col))
  :rule-classes :type-prescription)

Theorem: vl-linecol->col-of-vl-linecol

(defthm vl-linecol->col-of-vl-linecol
  (equal (vl-linecol->col (vl-linecol line col))
         (nfix col)))