		Search-engine friendly clone of the ACL2 documentation.

Validation-information

Code-ensemble-annop

Check if a code ensemble is annotated with validation information.

Signature
(code-ensemble-annop code) → yes/no
Arguments: code — Guard (code-ensemblep code).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: code-ensemble-annop

(defun code-ensemble-annop (code)
  (declare (xargs :guard (code-ensemblep code)))
  (let ((__function__ 'code-ensemble-annop))
    (declare (ignorable __function__))
    (transunit-ensemble-annop (code-ensemble->transunits code))))

Theorem: booleanp-of-code-ensemble-annop

(defthm booleanp-of-code-ensemble-annop
  (b* ((yes/no (code-ensemble-annop code)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: code-ensemble-annop-of-code-ensemble-fix-code

(defthm code-ensemble-annop-of-code-ensemble-fix-code
  (equal (code-ensemble-annop (code-ensemble-fix code))
         (code-ensemble-annop code)))

Theorem: code-ensemble-annop-code-ensemble-equiv-congruence-on-code

(defthm code-ensemble-annop-code-ensemble-equiv-congruence-on-code
  (implies (code-ensemble-equiv code code-equiv)
           (equal (code-ensemble-annop code)
                  (code-ensemble-annop code-equiv)))
  :rule-classes :congruence)