		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Transunit-formalp

Check if a translation unit has formal dynamic semantics.

Signature
(transunit-formalp tunit) → yes/no
Arguments: tunit — Guard (transunitp tunit).
Returns: yes/no — Type (booleanp yes/no).

All its external declarations must be supported.

Definitions and Theorems

Function: transunit-formalp

(defun transunit-formalp (tunit)
  (declare (xargs :guard (transunitp tunit)))
  (declare (xargs :guard (transunit-unambp tunit)))
  (let ((__function__ 'transunit-formalp))
    (declare (ignorable __function__))
    (extdecl-list-formalp (transunit->decls tunit))))

Theorem: booleanp-of-transunit-formalp

(defthm booleanp-of-transunit-formalp
  (b* ((yes/no (transunit-formalp tunit)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: transunit-formalp-of-transunit-fix-tunit

(defthm transunit-formalp-of-transunit-fix-tunit
  (equal (transunit-formalp (transunit-fix tunit))
         (transunit-formalp tunit)))

Theorem: transunit-formalp-transunit-equiv-congruence-on-tunit

(defthm transunit-formalp-transunit-equiv-congruence-on-tunit
  (implies (transunit-equiv tunit tunit-equiv)
           (equal (transunit-formalp tunit)
                  (transunit-formalp tunit-equiv)))
  :rule-classes :congruence)