		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-make-initial-defines

Simple way to build a vl-defines-p that `defines a list of names to 1.

Signature
(vl-make-initial-defines x &key stickyp) → defs
Arguments: x — Guard (string-listp x).; stickyp — Guard (booleanp stickyp).
Returns: defs — Type (vl-defines-p defs).

Definitions and Theorems

Function: vl-make-initial-defines-fn

(defun vl-make-initial-defines-fn (x stickyp)
  (declare (xargs :guard (and (string-listp x)
                              (booleanp stickyp))))
  (let ((__function__ 'vl-make-initial-defines))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (vl-add-define (car x)
                     (make-vl-define :formals nil
                                     :body "1"
                                     :loc *vl-fakeloc*
                                     :stickyp stickyp)
                     (vl-make-initial-defines (cdr x)
                                              :stickyp stickyp)))))

Theorem: vl-defines-p-of-vl-make-initial-defines

(defthm vl-defines-p-of-vl-make-initial-defines
  (b* ((defs (vl-make-initial-defines-fn x stickyp)))
    (vl-defines-p defs))
  :rule-classes :rewrite)

Theorem: vl-make-initial-defines-fn-of-string-list-fix-x

(defthm vl-make-initial-defines-fn-of-string-list-fix-x
  (equal (vl-make-initial-defines-fn (string-list-fix x)
                                     stickyp)
         (vl-make-initial-defines-fn x stickyp)))

Theorem: vl-make-initial-defines-fn-string-list-equiv-congruence-on-x

(defthm vl-make-initial-defines-fn-string-list-equiv-congruence-on-x
  (implies (str::string-list-equiv x x-equiv)
           (equal (vl-make-initial-defines-fn x stickyp)
                  (vl-make-initial-defines-fn x-equiv stickyp)))
  :rule-classes :congruence)

Theorem: vl-make-initial-defines-fn-of-bool-fix-stickyp

(defthm vl-make-initial-defines-fn-of-bool-fix-stickyp
  (equal (vl-make-initial-defines-fn x (acl2::bool-fix stickyp))
         (vl-make-initial-defines-fn x stickyp)))

Theorem: vl-make-initial-defines-fn-iff-congruence-on-stickyp

(defthm vl-make-initial-defines-fn-iff-congruence-on-stickyp
  (implies (iff stickyp stickyp-equiv)
           (equal (vl-make-initial-defines-fn x stickyp)
                  (vl-make-initial-defines-fn x stickyp-equiv)))
  :rule-classes :congruence)