		Search-engine friendly clone of the ACL2 documentation.

Cblock-path-checking

Vl-cblocks-synth

Signature
(vl-cblocks-synth x vars delta) → (mv delta cvtregs)
Arguments: x — Guard (vl-alwayslist-p x).; vars — Guard (vl-vardecllist-p vars).; delta — Guard (vl-delta-p delta).
Returns: delta — Type (vl-delta-p delta), given the guard.; cvtregs — Type (string-listp cvtregs).

Definitions and Theorems

Function: vl-cblocks-synth

(defun vl-cblocks-synth (x vars delta)
  (declare (xargs :guard (and (vl-alwayslist-p x)
                              (vl-vardecllist-p vars)
                              (vl-delta-p delta))))
  (let ((__function__ 'vl-cblocks-synth))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv delta nil))
         ((mv delta cvtregs1)
          (vl-cblock-synth (car x) vars delta))
         ((mv delta cvtregs2)
          (vl-cblocks-synth (cdr x) vars delta)))
      (mv delta (append cvtregs1 cvtregs2)))))

Theorem: vl-delta-p-of-vl-cblocks-synth.delta

(defthm vl-delta-p-of-vl-cblocks-synth.delta
  (implies (and (force (vl-alwayslist-p x))
                (force (vl-vardecllist-p vars))
                (force (vl-delta-p delta)))
           (b* (((mv ?delta ?cvtregs)
                 (vl-cblocks-synth x vars delta)))
             (vl-delta-p delta)))
  :rule-classes :rewrite)

Theorem: string-listp-of-vl-cblocks-synth.cvtregs

(defthm string-listp-of-vl-cblocks-synth.cvtregs
  (b* (((mv ?delta ?cvtregs)
        (vl-cblocks-synth x vars delta)))
    (string-listp cvtregs))
  :rule-classes :rewrite)