		Search-engine friendly clone of the ACL2 documentation.

Nedgeflop

Vl-nedgeflop-or-edges

Signature
(vl-nedgeflop-or-edges edges) → x
Arguments: edges — Guard (vl-exprlist-p edges).
Returns: x — Type (vl-expr-p x), given the guard.

Definitions and Theorems

Function: vl-nedgeflop-or-edges

(defun vl-nedgeflop-or-edges (edges)
 (declare (xargs :guard (vl-exprlist-p edges)))
 (declare (xargs :guard (consp edges)))
 (let ((__function__ 'vl-nedgeflop-or-edges))
  (declare (ignorable __function__))
  (if (atom (cdr edges))
      (car edges)
   (make-vl-nonatom :op :vl-binary-bitor
                    :args (list (car edges)
                                (vl-nedgeflop-or-edges (cdr edges)))
                    :finalwidth 1
                    :finaltype :vl-unsigned))))

Theorem: vl-expr-p-of-vl-nedgeflop-or-edges

(defthm vl-expr-p-of-vl-nedgeflop-or-edges
  (implies (and (vl-exprlist-p edges)
                (consp edges))
           (b* ((x (vl-nedgeflop-or-edges edges)))
             (vl-expr-p x)))
  :rule-classes :rewrite)