		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-maybe-strip-outer-linestart

Signature
(vl-maybe-strip-outer-linestart x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

Definitions and Theorems

Function: vl-maybe-strip-outer-linestart

(defun vl-maybe-strip-outer-linestart (x)
 (declare (xargs :guard (vl-expr-p x)))
 (let ((__function__ 'vl-maybe-strip-outer-linestart))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x)))
   (vl-expr-case
    x :vl-unary
    (if (assoc-equal "VL_LINESTART" x.atts)
        (change-vl-unary x
                         :atts (vl-remove-keys '("VL_LINESTART")
                                               x.atts))
      x)
    :vl-binary
    (change-vl-binary x
                      :left (vl-maybe-strip-outer-linestart x.left))
    :vl-qmark
    (change-vl-qmark x
                     :test (vl-maybe-strip-outer-linestart x.test))
    :vl-mintypmax
    (change-vl-mintypmax
         x
         :min (vl-maybe-strip-outer-linestart x.min))
    :vl-cast x
    :vl-inside x :vl-eventexpr x :otherwise
    (b* ((x.atts (vl-expr->atts x)))
      (if (assoc-equal "VL_LINESTART" x.atts)
          (vl-expr-update-atts x
                               (vl-remove-keys '("VL_LINESTART")
                                               x.atts))
        x))))))

Theorem: vl-expr-p-of-vl-maybe-strip-outer-linestart

(defthm vl-expr-p-of-vl-maybe-strip-outer-linestart
  (b* ((new-x (vl-maybe-strip-outer-linestart x)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: vl-expr-count-of-vl-maybe-strip-outer-linestart

(defthm vl-expr-count-of-vl-maybe-strip-outer-linestart
  (b* nil
    (<= (vl-expr-count (vl-maybe-strip-outer-linestart x))
        (vl-expr-count x)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: vl-maybe-strip-outer-linestart-of-vl-expr-fix-x

(defthm vl-maybe-strip-outer-linestart-of-vl-expr-fix-x
  (equal (vl-maybe-strip-outer-linestart (vl-expr-fix x))
         (vl-maybe-strip-outer-linestart x)))

Theorem: vl-maybe-strip-outer-linestart-vl-expr-equiv-congruence-on-x

(defthm vl-maybe-strip-outer-linestart-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-maybe-strip-outer-linestart x)
                  (vl-maybe-strip-outer-linestart x-equiv)))
  :rule-classes :congruence)