		Search-engine friendly clone of the ACL2 documentation.

Vl-delta

Vl-delta-p

Recognizer for vl-delta structures.

Signature
(vl-delta-p x) → *

Definitions and Theorems

Function: vl-delta-p

(defun vl-delta-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'vl-delta-p))
  (declare (ignorable __function__))
  (and
    (std::prod-consp x)
    (std::prod-consp (std::prod-car x))
    (std::prod-consp (std::prod-cdr (std::prod-car x)))
    (std::prod-consp (std::prod-cdr x))
    (std::prod-consp (std::prod-car (std::prod-cdr x)))
    (std::prod-consp (std::prod-cdr (std::prod-cdr x)))
    (b*
      ((nf (std::prod-car (std::prod-car x)))
       (vardecls (std::prod-car (std::prod-cdr (std::prod-car x))))
       (assigns (std::prod-cdr (std::prod-cdr (std::prod-car x))))
       (modinsts (std::prod-car (std::prod-car (std::prod-cdr x))))
       (gateinsts (std::prod-cdr (std::prod-car (std::prod-cdr x))))
       (warnings (std::prod-car (std::prod-cdr (std::prod-cdr x))))
       (addmods (std::prod-cdr (std::prod-cdr (std::prod-cdr x)))))
      (and (vl-namefactory-p nf)
           (vl-vardecllist-p vardecls)
           (vl-assignlist-p assigns)
           (vl-modinstlist-p modinsts)
           (vl-gateinstlist-p gateinsts)
           (vl-warninglist-p warnings)
           (vl-modulelist-p addmods))))))

Subtopics

Vl-warn-delta: Add a warning to a delta.
Vl-starting-delta: Build an initial vl-delta-p for the module x.
Vl-free-delta: Frees the namefactory within a vl-delta-p and returns delta.
Dwarn: Make a vl-warning-p and add it to a vl-delta-p.