		Search-engine friendly clone of the ACL2 documentation.

Output-checking

Check-output-file

Check an output file.

Signature
(check-output-file outfile env) → type
Arguments: outfile — Guard (output-filep outfile).; env — Guard (senvp env).
Returns: type — Type (type-resultp type).

We check the underlying output section.

Definitions and Theorems

Function: check-output-file

(defun check-output-file (outfile env)
  (declare (xargs :guard (and (output-filep outfile)
                              (senvp env))))
  (let ((__function__ 'check-output-file))
    (declare (ignorable __function__))
    (check-output-section (output-file->get outfile)
                          env)))

Theorem: type-resultp-of-check-output-file

(defthm type-resultp-of-check-output-file
  (b* ((type (check-output-file outfile env)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-output-file-of-output-file-fix-outfile

(defthm check-output-file-of-output-file-fix-outfile
  (equal (check-output-file (output-file-fix outfile)
                            env)
         (check-output-file outfile env)))

Theorem: check-output-file-output-file-equiv-congruence-on-outfile

(defthm check-output-file-output-file-equiv-congruence-on-outfile
  (implies (output-file-equiv outfile outfile-equiv)
           (equal (check-output-file outfile env)
                  (check-output-file outfile-equiv env)))
  :rule-classes :congruence)

Theorem: check-output-file-of-senv-fix-env

(defthm check-output-file-of-senv-fix-env
  (equal (check-output-file outfile (senv-fix env))
         (check-output-file outfile env)))

Theorem: check-output-file-senv-equiv-congruence-on-env

(defthm check-output-file-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (check-output-file outfile env)
                  (check-output-file outfile env-equiv)))
  :rule-classes :congruence)