		Search-engine friendly clone of the ACL2 documentation.

Ascii-identifiers

Code-ensemble-aidentp

Check if a code ensemble only uses, in its translation unit ensemble, ASCII identifiers.

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

The condition is checked w.r.t. the GCC flag in the implementation environment.

Definitions and Theorems

Function: code-ensemble-aidentp

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

Theorem: booleanp-of-code-ensemble-aidentp

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

Theorem: code-ensemble-aidentp-of-code-ensemble-fix-code

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

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

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