		Search-engine friendly clone of the ACL2 documentation.

Tokens

Vl-token->breakp

Identify whether a token was the first token on a line.

Signature
(vl-token->breakp x) → breakp
Arguments: x — Guard (vl-token-p x).
Returns: breakp — Type (booleanp breakp).

Definitions and Theorems

Function: vl-token->breakp$inline

(defun vl-token->breakp$inline (x)
  (declare (xargs :guard (vl-token-p x)))
  (let ((__function__ 'vl-token->breakp))
    (declare (ignorable __function__))
    (mbe :logic
         (if (cond ((vl-inttoken-p x)
                    (vl-inttoken->breakp x))
                   ((vl-idtoken-p x)
                    (vl-idtoken->breakp x))
                   ((vl-sysidtoken-p x)
                    (vl-sysidtoken->breakp x))
                   ((vl-stringtoken-p x)
                    (vl-stringtoken->breakp x))
                   ((vl-realtoken-p x)
                    (vl-realtoken->breakp x))
                   ((vl-timetoken-p x)
                    (vl-timetoken->breakp x))
                   ((vl-extinttoken-p x)
                    (vl-extinttoken->breakp x))
                   ((vl-plaintoken-p x)
                    (vl-plaintoken->breakp x)))
             t
           nil)
         :exec (case (tag x)
                     (:vl-inttoken (cddddr x))
                     ((:vl-idtoken :vl-sysidtoken
                                   :vl-stringtoken :vl-timetoken)
                      (cdddr x))
                     (:vl-extinttoken (caddr x))
                     (otherwise (cddr x))))))

Theorem: booleanp-of-vl-token->breakp

(defthm booleanp-of-vl-token->breakp
  (b* ((breakp (vl-token->breakp$inline x)))
    (booleanp breakp))
  :rule-classes :type-prescription)