		Search-engine friendly clone of the ACL2 documentation.

Vl-lint

Vl-lintconfig-loadconfig

Signature
(vl-lintconfig-loadconfig config defines) → loadconfig
Arguments: config — Guard (vl-lintconfig-p config).; defines — Guard (vl-defines-p defines).
Returns: loadconfig — Type (vl-loadconfig-p loadconfig).

Definitions and Theorems

Function: vl-lintconfig-loadconfig

(defun vl-lintconfig-loadconfig (config defines)
  (declare (xargs :guard (and (vl-lintconfig-p config)
                              (vl-defines-p defines))))
  (let ((__function__ 'vl-lintconfig-loadconfig))
    (declare (ignorable __function__))
    (b* (((vl-lintconfig config)))
      (make-vl-loadconfig :edition config.edition
                          :strictp config.strict
                          :start-files config.start-files
                          :search-path config.search-path
                          :search-exts config.search-exts
                          :include-dirs config.include-dirs
                          :plusargs config.plusargs
                          :defines defines
                          :mintime 1/100
                          :debugp config.debug))))

Theorem: vl-loadconfig-p-of-vl-lintconfig-loadconfig

(defthm vl-loadconfig-p-of-vl-lintconfig-loadconfig
  (b* ((loadconfig (vl-lintconfig-loadconfig config defines)))
    (vl-loadconfig-p loadconfig))
  :rule-classes :rewrite)