		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-fileset

Check a file set.

Signature
(check-fileset fileset) → wf
Arguments: fileset — Guard (filesetp fileset).
Returns: wf — Type (wellformed-resultp wf).

First we preprocess the file set. If preprocessing is successful, we check the translation unit.

Definitions and Theorems

Function: check-fileset

(defun check-fileset (fileset)
  (declare (xargs :guard (filesetp fileset)))
  (let ((__function__ 'check-fileset))
    (declare (ignorable __function__))
    (b* (((okf tunit) (preprocess fileset)))
      (check-transunit tunit))))

Theorem: wellformed-resultp-of-check-fileset

(defthm wellformed-resultp-of-check-fileset
  (b* ((wf (check-fileset fileset)))
    (wellformed-resultp wf))
  :rule-classes :rewrite)

Theorem: check-fileset-of-fileset-fix-fileset

(defthm check-fileset-of-fileset-fix-fileset
  (equal (check-fileset (fileset-fix fileset))
         (check-fileset fileset)))

Theorem: check-fileset-fileset-equiv-congruence-on-fileset

(defthm check-fileset-fileset-equiv-congruence-on-fileset
  (implies (fileset-equiv fileset fileset-equiv)
           (equal (check-fileset fileset)
                  (check-fileset fileset-equiv)))
  :rule-classes :congruence)