		Search-engine friendly clone of the ACL2 documentation.

Portable-ascii-identifiers

Paident-stringp

Check if an ACL2 string is a portable ASCII identifier.

Signature
(paident-stringp str) → yes/no
Arguments: str — Guard (stringp str).
Returns: yes/no — Type (booleanp yes/no).

For now we only check distinctness with the C17 keywords, but we plan to generalize that to other C versions.

Definitions and Theorems

Function: paident-stringp

(defun paident-stringp (str)
  (declare (xargs :guard (stringp str)))
  (and (paident-char-listp (acl2::explode str))
       (not (member-equal (str-fix str)
                          *keywords-c17*))))

Theorem: booleanp-of-paident-stringp

(defthm booleanp-of-paident-stringp
  (b* ((yes/no (paident-stringp str)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: paident-stringp-of-str-fix-str

(defthm paident-stringp-of-str-fix-str
  (equal (paident-stringp (str-fix str))
         (paident-stringp str)))

Theorem: paident-stringp-streqv-congruence-on-str

(defthm paident-stringp-streqv-congruence-on-str
  (implies (acl2::streqv str str-equiv)
           (equal (paident-stringp str)
                  (paident-stringp str-equiv)))
  :rule-classes :congruence)