		Search-engine friendly clone of the ACL2 documentation.

Parse-expressions

Vl-extend-expr-with-linestart

Signature
(vl-extend-expr-with-linestart linestart expr) → new-expr
Arguments: linestart — Guard (maybe-natp linestart).; expr — Guard (vl-expr-p expr).
Returns: new-expr — Type (vl-expr-p new-expr).

Definitions and Theorems

Function: vl-extend-expr-with-linestart

(defun vl-extend-expr-with-linestart (linestart expr)
  (declare (xargs :guard (and (maybe-natp linestart)
                              (vl-expr-p expr))))
  (let ((__function__ 'vl-extend-expr-with-linestart))
    (declare (ignorable __function__))
    (b* ((expr (vl-expr-fix expr))
         ((unless linestart) expr)
         (atts (vl-expr->atts expr))
         (atts (vl-extend-atts-with-linestart linestart atts)))
      (vl-expr-update-atts expr atts))))

Theorem: vl-expr-p-of-vl-extend-expr-with-linestart

(defthm vl-expr-p-of-vl-extend-expr-with-linestart
  (b* ((new-expr (vl-extend-expr-with-linestart linestart expr)))
    (vl-expr-p new-expr))
  :rule-classes :rewrite)