		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->gcc

Flag saying whether GCC extensions are supported or not.

Signature
(ppstate->gcc ppstate) → gcc
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: gcc — Type (booleanp gcc).

Definitions and Theorems

Function: ppstate->gcc

(defun ppstate->gcc (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (ppstatep ppstate)))
  (c::version-gccp (ppstate->version ppstate)))

Theorem: booleanp-of-ppstate->gcc

(defthm booleanp-of-ppstate->gcc
  (b* ((gcc (ppstate->gcc ppstate)))
    (booleanp gcc))
  :rule-classes :rewrite)

Theorem: ppstate->gcc-of-ppstate-fix-ppstate

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

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

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