		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Ienv->gcc

Flag saying whether GCC extensions are enabled or not.

Signature
(ienv->gcc ienv) → yes/no
Arguments: ienv — Guard (ienvp ienv).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: ienv->gcc

(defun ienv->gcc (ienv)
  (declare (xargs :guard (ienvp ienv)))
  (c::version-gccp (ienv->version ienv)))

Theorem: booleanp-of-ienv->gcc

(defthm booleanp-of-ienv->gcc
  (b* ((yes/no (ienv->gcc ienv)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ienv->gcc-of-ienv-fix-ienv

(defthm ienv->gcc-of-ienv-fix-ienv
  (equal (ienv->gcc (ienv-fix ienv))
         (ienv->gcc ienv)))

Theorem: ienv->gcc-ienv-equiv-congruence-on-ienv

(defthm ienv->gcc-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (ienv->gcc ienv)
                  (ienv->gcc ienv-equiv)))
  :rule-classes :congruence)