		Search-engine friendly clone of the ACL2 documentation.

Syntax

Vl-distweighttype-p

Representation of the := or :/ weight operators.

See SystemVerilog-2012 Section 18.5.4, Distribution, and also see vl-distitem.

:vl-weight-each stands for the := operator, which assigns the same weight to each item in the range.
:vl-weight-total stands for the :/ operator, which assigns a weight to the range as a whole, i.e., the weight of each value in the range will become weight/n where n is the number of items in the range.

Both operators have the same meaning when applied to a single expression instead of a range.

This is an ordinary defenum.

Function: vl-distweighttype-p

(defun vl-distweighttype-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-weight-each)
      (eq x ':vl-weight-total)))

Theorem: type-when-vl-distweighttype-p

(defthm type-when-vl-distweighttype-p
  (implies (vl-distweighttype-p x)
           (if (symbolp x)
               (if (not (equal x 't))
                   (not (equal x 'nil))
                 'nil)
             'nil))
  :rule-classes :compound-recognizer)