		Search-engine friendly clone of the ACL2 documentation.

Expressions

Vl-expr->finalwidth

Get the finalwidth from an expression.

Signature
(vl-expr->finalwidth x) → width?
Arguments: x — Guard (vl-expr-p x).
Returns: width? — Type (maybe-natp width?).

See vl-expr-p for a discussion of widths. The result is a maybe-natp.

Definitions and Theorems

Function: vl-expr->finalwidth$inline

(defun vl-expr->finalwidth$inline (x)
  (declare (xargs :guard (vl-expr-p x)))
  (let ((__function__ 'vl-expr->finalwidth))
    (declare (ignorable __function__))
    (vl-expr-case x
                  :atom x.finalwidth
                  :nonatom x.finalwidth)))

Theorem: maybe-natp-of-vl-expr->finalwidth

(defthm maybe-natp-of-vl-expr->finalwidth
  (b* ((width? (vl-expr->finalwidth$inline x)))
    (maybe-natp width?))
  :rule-classes :type-prescription)

Theorem: vl-expr->finalwidth-of-vl-atom

(defthm vl-expr->finalwidth-of-vl-atom
  (equal (vl-expr->finalwidth (make-vl-atom :guts guts
                                            :finalwidth finalwidth
                                            :finaltype finaltype
                                            :atts atts))
         (maybe-natp-fix finalwidth)))

Theorem: vl-expr->finalwidth-of-vl-nonatom

(defthm vl-expr->finalwidth-of-vl-nonatom
 (equal (vl-expr->finalwidth (make-vl-nonatom :op op
                                              :atts atts
                                              :args args
                                              :finalwidth finalwidth
                                              :finaltype finaltype))
        (maybe-natp-fix finalwidth)))

Theorem: vl-expr->finalwidth$inline-of-vl-expr-fix-x

(defthm vl-expr->finalwidth$inline-of-vl-expr-fix-x
  (equal (vl-expr->finalwidth$inline (vl-expr-fix x))
         (vl-expr->finalwidth$inline x)))

Theorem: vl-expr->finalwidth$inline-vl-expr-equiv-congruence-on-x

(defthm vl-expr->finalwidth$inline-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr->finalwidth$inline x)
                  (vl-expr->finalwidth$inline x-equiv)))
  :rule-classes :congruence)