		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).

Definitions and Theorems

Function: paident-stringp

(defun paident-stringp (str)
  (declare (xargs :guard (stringp str)))
  (let ((__function__ 'paident-stringp))
    (declare (ignorable __function__))
    (and (paident-char-listp (acl2::explode str))
         (not (member-equal str *keywords*)))))

Theorem: booleanp-of-paident-stringp

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