		Search-engine friendly clone of the ACL2 documentation.

Versions

Version-std-c17p

Check if the C standard for this C version is C17.

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

That is, check whether the C version is C17, with or without GCC extensions.

Definitions and Theorems

Function: version-std-c17p

(defun version-std-c17p (version)
  (declare (xargs :guard (versionp version)))
  (or (version-case version :c17)
      (version-case version :c17+gcc)))

Theorem: booleanp-of-version-std-c17p

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

Theorem: version-std-c17p-of-version-fix-version

(defthm version-std-c17p-of-version-fix-version
  (equal (version-std-c17p (version-fix version))
         (version-std-c17p version)))

Theorem: version-std-c17p-version-equiv-congruence-on-version

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