		Search-engine friendly clone of the ACL2 documentation.

Vl-linecol

Vl-linecol->line

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

Definitions and Theorems

Function: vl-linecol->line$inline

(defun vl-linecol->line$inline (x)
  (declare (xargs :guard (vl-linecol-p x)))
  (let ((__function__ 'vl-linecol->line))
    (declare (ignorable __function__))
    (b* ((x (vl-linecol-fix x))
         ((when (consp x)) (car x)))
      (the (unsigned-byte 30)
           (ash (the (unsigned-byte 52) x) -22)))))

Theorem: posp-of-vl-linecol->line

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

Theorem: vl-linecol->line-of-vl-linecol

(defthm vl-linecol->line-of-vl-linecol
  (equal (vl-linecol->line (vl-linecol line col))
         (pos-fix line)))