		Search-engine friendly clone of the ACL2 documentation.

Versions

Version-gccp

Check if this C version includes GCC extensions or not.

Signature
(version-gccp version) → yes/no
Arguments: version — Guard (versionp version).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: version-gccp

(defun version-gccp (version)
  (declare (xargs :guard (versionp version)))
  (or (version-case version :c17+gcc)
      (version-case version :c23+gcc)))

Theorem: booleanp-of-version-gccp

(defthm booleanp-of-version-gccp
  (b* ((yes/no (version-gccp version)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: version-gccp-of-version-fix-version

(defthm version-gccp-of-version-fix-version
  (equal (version-gccp (version-fix version))
         (version-gccp version)))

Theorem: version-gccp-version-equiv-congruence-on-version

(defthm version-gccp-version-equiv-congruence-on-version
  (implies (version-equiv version version-equiv)
           (equal (version-gccp version)
                  (version-gccp version-equiv)))
  :rule-classes :congruence)