		Search-engine friendly clone of the ACL2 documentation.

Numbered-name-index-end

Numbered-name-index-end-p

Recognize admissible ending markers of the numeric index of numbered names.

Signature
(numbered-name-index-end-p x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Check whether x consists of zero or more non-numeric characters.

Definitions and Theorems

Function: numbered-name-index-end-p

(defun numbered-name-index-end-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'numbered-name-index-end-p))
    (declare (ignorable __function__))
    (and (stringp x)
         (str::nondigit-charlist-p (explode x)))))

Theorem: booleanp-of-numbered-name-index-end-p

(defthm booleanp-of-numbered-name-index-end-p
  (b* ((yes/no (numbered-name-index-end-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)